Computational types from a logical perspective

DOI10.1017/S0956796898002998zbMath0920.03023OpenAlexW1981311833WikidataQ56210999 ScholiaQ56210999MaRDI QIDQ4236755

G. M. Bierman, P. N. Benton, V. C. V. de Paiva

Publication date: 18 May 1999

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796898002998

zbMATH Keywords

sequent calculusnatural deductionconfluenceKripke modelscategorical modelscartesian closed categorystrong normalisationterm calculusstrong monadcomputational lambda calculusHilbert-style presentationsintuitionistic modal propositional logicmetalanguage for denotational semantics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items

Kleene Monads: Handling Iteration in a Framework of Generic Effects ⋮ The Došen square under construction: a tale of four modalities ⋮ Control effects as a modality ⋮ Logic in Access Control (Tutorial Notes) ⋮ Embedding Constructive K into Intuitionistic K ⋮ Unnamed Item ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Intuitionistic conditional logics ⋮ Admissible rules for six intuitionistic modal logics ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ The Cooper storage idiom ⋮ Mathematical modal logic: A view of its evolution ⋮ Linearity, Control Effects, and Behavioral Types ⋮ A semantic hierarchy for intuitionistic logic ⋮ Fibrational modal type theory ⋮ A generic complete dynamic logic for reasoning about purity and effects ⋮ A general method for proving decidability of intuitionistic modal logics ⋮ 1999 European Summer Meeting of the Association for Symbolic Logic ⋮ Unnamed Item ⋮ A Kuroda-style \(j\)-translation ⋮ Cut-free Gentzen calculus for multimodal CK ⋮ Constructive Modalities with Provability Smack

This page was built for publication: Computational types from a logical perspective