Kripke-style models for typed lambda calculus

DOI10.1016/0168-0072(91)90067-VMaRDI QIDQ804559zbMATH OpenFDO

Authors John Mitchell, Eugenio Moggi

Publication date 1991

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

semanticsCartesian closed categoriestyped lambda calculusKripke modelHenkin modellogical relations over Kripke structures

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Recommendations

• scientific article; zbMATH DE number 4103048
• Kripke models and the (in)equational logic of the second-order -calculus
• A simple class of Kripke-style models in which logic and computation have equal standing
• scientific article; zbMATH DE number 3941502
• scientific article; zbMATH DE number 3941503

Cites work

• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 3936506 (Why is no real title available?)
• scientific article; zbMATH DE number 3949678 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 3784848 (Why is no real title available?)
• scientific article; zbMATH DE number 3485758 (Why is no real title available?)
• scientific article; zbMATH DE number 3556025 (Why is no real title available?)
• scientific article; zbMATH DE number 1988959 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3342819 (Why is no real title available?)
• Completeness in the theory of types
• Completeness, invariance and λ-definability
• Harvey Friedman's research on the foundations of mathematics
• Logical relations and the typed λ-calculus
• Open maps of toposes
• Recursive models for constructive set theories
• What is a model of the lambda calculus?

Cited in

(28)

• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Prelogical relations
• Kripke semantics for higher-order type theory applied to constraint logic programming languages
• Categorical reconstruction of a reduction free normalization proof
• scientific article; zbMATH DE number 4103048 (Why is no real title available?)
• A semantics for Prolog
• Mechanized metatheory revisited
• Linear Läuchli semantics
• Equality between functionals in the presence of coproducts
• A logic for repair and state recovery in Byzantine fault-tolerant multi-agent systems
• Cryptographic logical relations
• The semantics of second-order lambda calculus
• Simplicial models for the epistemic logic of faulty agents
• A simple class of Kripke-style models in which logic and computation have equal standing
• Intersection and union types
• Substitution structures
• Completeness of type assignment systems with intersection, union, and type quantifiers
• POPLMark reloaded: mechanizing proofs by logical relations
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Kripke models and the (in)equational logic of the second-order -calculus
• Kripke Semantics for Martin-Löf’s Extensional Type Theory
• Abstract deduction and inferential models for type theory
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• Proof-search in type-theoretic languages: An introduction
• Bunched polymorphism
• A characterization of lambda definability in categorical models of implicit polymorphism
• A weakly initial algebra for higher-order abstract syntax in Cedille
• A Survey of the Proof-Theoretic Foundations of Logic Programming

This page was built for publication: Kripke-style models for typed lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q804559)