Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus

DOI10.1016/S0168-0072(96)00039-5zbMath0873.03017OpenAlexW1985397485MaRDI QIDQ1356979

Jean H. Gallier

Publication date: 16 June 1997

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

Full work available at URL: https://doi.org/10.1016/s0168-0072(96)00039-5

zbMATH Keywords

inequalitiescompletenessKripke modelsproof systemssoundnessequationsCartesian-closed categoryrewrite rulestype abstractioncategory of preordersexponential of functorssecond-order \(\lambda\)-calculus

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Extensional models for polymorphism
• Kripke-style models for typed lambda calculus
• The system \({\mathcal F}\) of variable types, fifteen years later
• Filter models with polymorphic types
• Sheaves in geometry and logic: a first introduction to topos theory
• A semantics for static type inference
• Categorical semantics for higher order polymorphic lambda calculus
• Completeness, invariance and λ-definability
• Completeness in the theory of types

This page was built for publication: Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus