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

DOI10.1016/0304-3975(94)00280-0zbMATH Open0873.68125OpenAlexW1971766620MaRDI QIDQ673628FDOQ673628

Authors: Jean 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

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

zbMATH Keywords

realizabilitycover algebra

Mathematics Subject Classification ID

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

Cites Work

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

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)