An interpretation of Martin-Löf's type theory in a type-free theory of propositions

DOI10.2307/2274128zbMath0618.03029OpenAlexW2089366670MaRDI QIDQ3754617

Jan Smith

Publication date: 1984

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2274128

zbMATH Keywords

Frege structureslambda-calculussemantic

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items

From type theory to setoids and back, Constructing recursion operators in intuitionistic type theory, Constructive system for automatic program synthesis, Domain interpretations of Martin-Löf's partial type theory, Optimized encodings of fragments of type theory in first order logic, Constructing type systems over an operational semantics, Towards a computation system based on set theory, Proof-search in type-theoretic languages: An introduction, MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK, Program Testing and the Meaning Explanations of Intuitionistic Type Theory