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)

Full work available at URL https://doi.org/10.1016/0168-0072(91)90067-V

zbMATH Keywords

Cartesian closed categoriesHenkin modelKripke modellogical relations over Kripke structuressemanticstyped lambda calculus

Mathematics Subject Classification ID

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

Review text

As an extension for usual Henkin models, Kripke-style models are defined for typed lambda calculus. As for the relationship between the models and Cartesian closed categories (CCCs), every Kripke model determines a CCC, and every small CCC may be embedded in a Kripke model. Kripke models are Cartesian closed subcategories of the presheaves over a poset. Strong completeness is proved for Kripke models: every set of equations that is closed under implication is the theory of a single Kripke model. Moreover, the notion of logical relations over Kripke structures is developed, showing that every theory is the theory of a model determined by a Kripke equivalence relation over a Henkin model.

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

• Completeness in the theory of types
• Completeness, invariance and λ-definability
• Harvey Friedman's research on the foundations of mathematics
• 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?)
• 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

(31)

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

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)