Computational types from a logical perspective
From MaRDI portal
cartesian closed categorycategorical modelscomputational lambda calculusconfluenceHilbert-style presentationsintuitionistic modal propositional logicKripke modelsmetalanguage for denotational semanticsnatural deductionsequent calculusstrong monadstrong normalisationterm calculus
Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Semantics in the theory of computing (68Q55)
Recommendations
Cited in
(57)- Computations on types
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
- Monad as modality
- Mathematical modal logic: A view of its evolution
- Fitch-style modal lambda calculi
- Lewis meets Brouwer: constructive strict implication
- The Cooper storage idiom
- A semantic hierarchy for intuitionistic logic
- Fibrational modal type theory
- Denotation of contextual modal type theory (CMTT): syntax and meta-programming
- Curry-Howard-Lambek correspondence for intuitionistic belief
- The Došen square under construction: a tale of four modalities
- Intuitionistic conditional logics
- A Kuroda-style \(j\)-translation
- A general method for proving decidability of intuitionistic modal logics
- Admissible rules for six intuitionistic modal logics
- On types and type consistency in logic programming (Diss., FernUniv. Hagen, 1999)
- Computing with semirings and weak rig groupoids
- Kleene monads: handling iteration in a framework of generic effects
- Linearity, control effects, and behavioral types
- Logic in Access Control (Tutorial Notes)
- Embedding constructive K into intuitionistic K
- scientific article; zbMATH DE number 4172407 (Why is no real title available?)
- scientific article; zbMATH DE number 3941502 (Why is no real title available?)
- scientific article; zbMATH DE number 1330443 (Why is no real title available?)
- scientific article; zbMATH DE number 742723 (Why is no real title available?)
- scientific article; zbMATH DE number 1088039 (Why is no real title available?)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- scientific article; zbMATH DE number 1497732 (Why is no real title available?)
- scientific article; zbMATH DE number 1522506 (Why is no real title available?)
- A Constructive Logic for Services and Information Flow in Computer Networks
- On the identity type as the type of computational paths
- scientific article; zbMATH DE number 756051 (Why is no real title available?)
- scientific article; zbMATH DE number 2085167 (Why is no real title available?)
- scientific article; zbMATH DE number 2110617 (Why is no real title available?)
- Basic constructive modality
- 1999 European Summer Meeting of the Association for Symbolic Logic
- Computational adequacy for substructural lambda calculi
- Problems in rewriting applied to categorical concepts by the example of a computational comonad
- How to prove decidability of equational theories with second-order computation analyser SOL
- Dual-context calculi for modal logic
- Constructive modalities with provability smack
- Control effects as a modality
- Modal Hilbert algebras and their triple representation
- From semantics to types: the case of the imperative \(\lambda\)-calculus
- Towards logical foundations for probabilistic computation
- Substructural nuclear (image-based) logics and operational Kripke-style semantics
- Curry and Howard meet Borel
- Adjoint natural deduction
- Twin procedures, two kinds of variable binding, and two kinds of computation
- Hyperintensions as computations
- The quantum monadology
- A monadic formalization of ML5
- Strong Normalization of Moggis's Computational Metalanguage
- Notions of computation and monads
- Cut-free Gentzen calculus for multimodal CK
- A generic complete dynamic logic for reasoning about purity and effects
This page was built for publication: Computational types from a logical perspective
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4236755)
