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

• Publication:3827990
• Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus
• A simple class of Kripke-style models in which logic and computation have equal standing
• Publication:3714050
• Publication:3714051

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

(26)

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

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)