Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
From MaRDI portal
Publication:673628
DOI10.1016/0304-3975(94)00280-0zbMath0873.68125OpenAlexW1971766620MaRDI QIDQ673628
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
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
