An information system interpretation of Martin-Löf's partial type theory with universes

DOI10.1006/INCO.1993.1048zbMATH Open0789.03045OpenAlexW1992671459MaRDI QIDQ1308982FDOQ1308982

Authors: Erik Palmgren 

Publication date: 14 June 1994

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1993.1048

Recommendations

• Domain interpretations of Martin-Löf's partial type theory
• Remarks on Martin-Löf's partial type theory
• scientific article; zbMATH DE number 65535
• A construction of type: type in Martin-Löf's partial type theory with one universe
• scientific article; zbMATH DE number 1302063

zbMATH Keywords

fixed point operatorcontinuous operatorsuniversesdomain-theoretic interpretationScott's information systemstype universe equationsMartin-Löf's partial type theory

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Second- and higher-order arithmetic and fragments (03F35)

Cited In (6)

• Inaccessibility in constructive set theory and type theory
• Hyperfinite type structures
• Remarks on Martin-Löf's partial type theory
• The constructive Hilbert program and the limits of Martin-Löf type theory
• Domain interpretations of Martin-Löf's partial type theory
• Information and knowledge. A constructive type-theoretical approach

This page was built for publication: An information system interpretation of Martin-Löf's partial type theory with universes

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