Remarks on Martin-Löf's partial type theory

DOI10.1007/BF01995109MaRDI QIDQ688734zbMATH OpenFDO

Authors Erik Palmgren, Viggo Stoltenberg-Hansen

Publication date 28 November 1993

Published in BIT (Search for Journal in Brave)

zbMATH Keywords

domainscategory of conditional upper semilattices and parametrizations thereoffixed point operatortype theory with general recursionMartin-Löf's partial type theory

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• An information system interpretation of Martin-Löf's partial type theory with universes
• Domain interpretations of Martin-Löf's partial type theory
• Recursion on the partial continuous functionals
• A construction of type: type in Martin-Löf's partial type theory with one universe
• HYBRID PARTIAL-TOTAL TYPE THEORY

Cites work

• scientific article; zbMATH DE number 5297230 (Why is no real title available?)
• scientific article; zbMATH DE number 3928338 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 4187805 (Why is no real title available?)
• A construction of type: type in Martin-Löf's partial type theory with one universe
• An information system interpretation of Martin-Löf's partial type theory with universes
• Domain interpretations of Martin-Löf's partial type theory
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes

Cited in

(17)

• scientific article; zbMATH DE number 1302058 (Why is no real title available?)
• Martin Hofmann’s contributions to type theory: Groupoids and univalence
• An information system interpretation of Martin-Löf's partial type theory with universes
• The Friedman‐Translation for Martin‐Löf's Type Theory
• Domain interpretations of Martin-Löf's partial type theory
• Kripke Semantics for Martin-Löf’s Extensional 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
• Partiality, state and dependent types
• An adequacy theorem for dependent type theory
• HYBRID PARTIAL-TOTAL TYPE THEORY
• On the strength of dependent products in the type theory of Martin-Löf
• Recursion on the partial continuous functionals
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• scientific article; zbMATH DE number 2003151 (Why is no real title available?)

This page was built for publication: Remarks on Martin-Löf's partial type theory

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