Recursive models for constructive set theories

DOI10.1016/0003-4843(82)90003-1zbMath0514.03039OpenAlexW1964913565MaRDI QIDQ3659782

Michael J. 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 mathematicsconstructive set theorylambda-calculusdata typeseffective operationsMartin-Loef's theory

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50)

Related Items (15)

The strength of some Martin-Löf type theories ⋮ Extensional realizability ⋮ Church's thesis, continuity, and set theory ⋮ Domain interpretations of Martin-Löf's partial type theory ⋮ Constructing type systems over an operational semantics ⋮ Semantics of constructions. I: The traditional approach ⋮ Inductive types and exact completion ⋮ Categorical and algebraic aspects of Martin-Löf type theory ⋮ The semantics of second-order lambda calculus ⋮ Functional interpretation of Aczel's constructive set theory ⋮ Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) ⋮ Some results on cut-elimination, provable well-orderings, induction and reflection ⋮ MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Kripke-style models for typed lambda calculus

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