Proving properties of typed -terms using realizability, covers, and sheaves

DOI10.1016/0304-3975(94)00280-0MaRDI QIDQ673628zbMATH OpenOpenAlexFDO

Authors Jean Gallier

Publication date 28 February 1997

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

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

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

zbMATH Keywords

realizabilitycover algebra

Mathematics Subject Classification ID

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

Recommendations

• A finite axiomatization of propositional type theory in pure lambda calculus
• scientific article; zbMATH DE number 512879
• scientific article; zbMATH DE number 1301734
• A semantic characterization of the well-typed formulae of \(\lambda\)- calculus
• A revised completeness result for the simply typed \(\lambda\mu\)-calculus using realizability semantics
• La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
• Linear realizability and full completeness for typed lambda-calculi
• Proof theory of constructive systems: inductive types and univalence

Cites work

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

Cited in

(3)

• Strong normalization for non-structural subtyping via saturated sets
• Typing untyped \(\lambda\)-terms, or reducibility strikes again!
• On the Stability by Union of Reducibility Candidates

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q673628)