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

DOI10.2307/2274128MaRDI QIDQ3754617zbMATH OpenOpenAlexFDO

Authors 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

semanticlambda-calculusFrege structures

Mathematics Subject Classification ID

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

Recommendations

• Characterizing the interpretation of set theory in Martin-Löf type theory
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• scientific article; zbMATH DE number 4027461
• Realizability and intuitionistic logic
• scientific article; zbMATH DE number 4096759

Cited in

(16)

• scientific article; zbMATH DE number 1302058 (Why is no real title available?)
• Constructing type systems over an operational semantics
• The Friedman‐Translation for Martin‐Löf's Type Theory
• Proof-search in type-theoretic languages: An introduction
• Constructive system for automatic program synthesis
• Domain interpretations of Martin-Löf's partial type theory
• From type theory to setoids and back
• Optimized encodings of fragments of type theory in first order logic
• Type-free property theory, exemplification and Russell's paradox
• Characterizing the interpretation of set theory in Martin-Löf type theory
• ERRATA: "The paper: MARTIN-LOF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK"
• Martin-Löf's type theory as an open-ended framework
• Program testing and the meaning explanations of intuitionistic type theory
• Towards a computation system based on set theory
• Constructing recursion operators in intuitionistic type theory
• scientific article; zbMATH DE number 4027461 (Why is no real title available?)

This page was built for publication: An interpretation of Martin-Löf's type theory in a type-free theory of propositions

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