Kripke-style models for typed lambda calculus

DOI10.1016/0168-0072(91)90067-VzbMath0728.03011MaRDI QIDQ804559

John C. Mitchell, Eugenio Moggi

Publication date: 1991

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

zbMATH Keywords

Cartesian closed categoriessemanticsKripke modeltyped lambda calculusHenkin modellogical relations over Kripke structures

Mathematics Subject Classification ID

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

Related Items

Fresh logic: Proof-theory and semantics for FM and nominal techniques, Categorical reconstruction of a reduction free normalization proof, A semantics for \(\lambda \)Prolog, Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus, Linear Läuchli semantics, Intersection and union types, A Survey of the Proof-Theoretic Foundations of Logic Programming, POPLMark reloaded: Mechanizing proofs by logical relations, Bunched polymorphism, A characterization of lambda definability in categorical models of implicit polymorphism, Kripke semantics for higher-order type theory applied to constraint logic programming languages, Cryptographic logical relations, Abstract deduction and inferential models for type theory, Completeness of type assignment systems with intersection, union, and type quantifiers, Substitution structures, The semantics of second-order lambda calculus, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance, Kripke Semantics for Martin-Löf’s Extensional Type Theory, Mechanized metatheory revisited, Proof-search in type-theoretic languages: An introduction, Equality between functionals in the presence of coproducts, Prelogical relations, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Cites Work

• Harvey Friedman's research on the foundations of mathematics
• Open maps of toposes
• Recursive models for constructive set theories
• Logical relations and the typed λ-calculus
• Completeness, invariance and λ-definability
• What is a model of the lambda calculus?
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item