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

DOI10.2307/2274128zbMATH Open0618.03029OpenAlexW2089366670MaRDI QIDQ3754617FDOQ3754617

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

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

zbMATH Keywords

semanticlambda-calculusFrege structures

Mathematics Subject Classification ID

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

Cited In (16)

• Characterizing the interpretation of set theory in Martin-Löf type theory
• Domain interpretations of Martin-Löf's partial type theory
• ERRATA: "The paper: MARTIN-LOF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK"
• The Friedman‐Translation for Martin‐Löf's Type Theory
• Program Testing and the Meaning Explanations of Intuitionistic Type Theory
• Constructing type systems over an operational semantics
• Optimized encodings of fragments of type theory in first order logic
• From type theory to setoids and back
• Title not available (Why is that?)
• Title not available (Why is that?)
• MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK
• Towards a computation system based on set theory
• Constructive system for automatic program synthesis
• Type-free property theory, exemplification and Russell's paradox
• Proof-search in type-theoretic languages: An introduction
• Constructing recursion operators in intuitionistic type theory

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)