Recursive models for constructive set theories

DOI10.1016/0003-4843(82)90003-1MaRDI QIDQ3659782zbMATH OpenOpenAlexFDO

Authors Michael Beeson

Publication date 1982

Published in Annals of Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0003-4843(82)90003-1

zbMATH Keywords

constructive mathematicslambda-calculusconstructive set theorydata typeseffective operationsMartin-Loef's theory

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50)

Cited in

(15)

• Kripke-style models for typed lambda calculus
• The strength of some Martin-Löf type theories
• Categorical and algebraic aspects of Martin-Löf type theory
• Domain interpretations of Martin-Löf's partial type theory
• Constructing type systems over an operational semantics
• Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
• Inductive types and exact completion
• Church's thesis, continuity, and set theory
• The semantics of second-order lambda calculus
• Program testing and the meaning explanations of intuitionistic type theory
• Functional interpretation of Aczel's constructive set theory
• Semantics of constructions. I: The traditional approach
• Extensional realizability
• Some results on cut-elimination, provable well-orderings, induction and reflection
• Martin-Löf's type theory as an open-ended framework

This page was built for publication: Recursive models for constructive set theories

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