Domain interpretations of Martin-Löf's partial type theory

DOI10.1016/0168-0072(90)90044-3MaRDI QIDQ916656zbMATH OpenOpenAlexFDO

Authors Erik Palmgren, Viggo Stoltenberg-Hansen

Publication date 1990

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(90)90044-3

zbMATH Keywords

consistently complete algebraic cpo'seffective continuous functioneffective continuous functoreffective domainoperational semantics of type theorypartial type theoryMartin-Löf type theory

Mathematics Subject Classification ID

Theory of numerations, effectively presented structures (03D45) Metamathematics of constructive systems (03F50) Continuous lattices and posets, applications (06B35) Semantics in the theory of computing (68Q55) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Remarks on Martin-Löf's partial type theory
• A type theoretic interpretation of constructive domain theory
• scientific article; zbMATH DE number 3853066
• scientific article; zbMATH DE number 1302058
• On the syntax of Martin-Löf's type theories
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• An information system interpretation of Martin-Löf's partial type theory with universes
• Kripke Semantics for Martin-Löf’s Extensional Type Theory
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• Characterizing the interpretation of set theory in Martin-Löf type theory

Cites work

• scientific article; zbMATH DE number 3817067 (Why is no real title available?)
• scientific article; zbMATH DE number 4027461 (Why is no real title available?)
• scientific article; zbMATH DE number 4050971 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Constructive mathematics and computer programming
• Domain theoretic models of polymorphism
• LCF considered as a programming language
• On the syntax of Martin-Löf's type theories
• Precision of double sampling estimators for comparing two probabilities
• Recursive models for constructive set theories
• The Category-Theoretic Solution of Recursive Domain Equations

Cited in

(21)

• scientific article; zbMATH DE number 1302058 (Why is no real title available?)
• scientific article; zbMATH DE number 1420788 (Why is no real title available?)
• Computational foundations of basic recursive function theory
• Well-ordering proofs for Martin-Löf type theory
• An information system interpretation of Martin-Löf's partial type theory with universes
• A type theoretic interpretation of constructive domain theory
• Remarks on Martin-Löf's partial type theory
• Formal definitions and proofs for partial (co)recursive functions
• A natural semantics of first-order type dependency
• Concrete models of computation for topological algebras
• Games for dependent types
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Kripke Semantics for Martin-Löf’s Extensional Type Theory
• Hyperfinite type structures
• The paradox of trees in type theory
• An adequacy theorem for dependent type theory
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• European Summer Meeting of the Association for Symbolic Logic, Uppsala 1991
• Game semantics for dependent types
• Game semantics of Martin-Löf type theory
• scientific article; zbMATH DE number 4027461 (Why is no real title available?)

This page was built for publication: Domain interpretations of 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 Q916656)