Remarks on Martin-Löf's partial type theory
From MaRDI portal
Publication:688734
DOI10.1007/BF01995109zbMATH Open0787.03051MaRDI QIDQ688734FDOQ688734
Authors: Erik Palmgren, Viggo Stoltenberg-Hansen 
Publication date: 28 November 1993
Published in: BIT (Search for Journal in Brave)
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
domainscategory of conditional upper semilattices and parametrizations thereoffixed point operatortype theory with general recursionMartin-Löf's partial type theory
Cites Work
- Title not available (Why is that?)
- The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
- Title not available (Why is that?)
- An information system interpretation of Martin-Löf's partial type theory with universes
- Title not available (Why is that?)
- Title not available (Why is that?)
- A construction of type: type in Martin-Löf's partial type theory with one universe
- Domain interpretations of Martin-Löf's partial type theory
Cited In (15)
- An adequacy theorem for dependent type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- An information system interpretation of Martin-Löf's partial type theory with universes
- 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
- HYBRID PARTIAL-TOTAL TYPE THEORY
- Title not available (Why is that?)
- Recursion on the partial continuous functionals
- Kripke Semantics for Martin-L\"of's Extensional Type Theory
- On the strength of dependent products in the type theory of Martin-Löf
- Title not available (Why is that?)
- Kripke Semantics for Martin-Löf’s Extensional Type Theory
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)
