Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves

DOI10.1016/0304-3975(94)00280-0zbMath0873.68125OpenAlexW1971766620MaRDI QIDQ673628

Jean H. Gallier

Publication date: 28 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)00280-0

zbMATH Keywords

realizabilitycover algebra

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Strong normalization for non-structural subtyping via saturated sets ⋮ Typing untyped \(\lambda\)-terms, or reducibility strikes again!

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Extensional models for polymorphism
• The system \({\mathcal F}\) of variable types, fifteen years later
• Filter models with polymorphic types
• Constructivism in mathematics. An introduction. Volume II
• Sheaves in geometry and logic: a first introduction to topos theory
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Church-Rosser theorem for typed functional systems
• Logical relations and the typed λ-calculus
• Forcing in intuitionistic systems without power-set
• Some lambda calculi with categorical sums and products
• Intensional interpretations of functionals of finite type I
• On the interpretation of intuitionistic number theory

This page was built for publication: Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves