Kripke-style models for typed lambda calculus

DOI10.1016/0168-0072(91)90067-VzbMATH Open0728.03011MaRDI QIDQ804559FDOQ804559

Authors: John Mitchell, Eugenio Moggi 

Publication date: 1991

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

Recommendations

• scientific article; zbMATH DE number 4103048
• 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
• scientific article; zbMATH DE number 3941502
• scientific article; zbMATH DE number 3941503

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)

Cites Work

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

Cited In (26)

• Prelogical relations
• Categorical reconstruction of a reduction free normalization proof
• Title not available (Why is that?)
• Kripke semantics for higher-order type theory applied to constraint logic programming languages
• A semantics for \(\lambda \)Prolog
• Mechanized metatheory revisited
• Linear Läuchli semantics
• Equality between functionals in the presence of coproducts
• POPLMark reloaded: Mechanizing proofs by logical relations
• Cryptographic logical relations
• Simplicial models for the epistemic logic of faulty agents
• The semantics of second-order lambda calculus
• 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
• 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 \(\lambda\)-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 Survey of the Proof-Theoretic Foundations of Logic Programming
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• A characterization of lambda definability in categorical models of implicit polymorphism

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)