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

DOI10.1016/0168-0072(90)90044-3zbMath0704.03041OpenAlexW2067618205MaRDI QIDQ916656

Viggo Stoltenberg-Hansen, Erik Palmgren

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

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

Mathematics Subject Classification ID

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

Related Items

Games for Dependent Types ⋮ Game semantics for dependent types ⋮ A type theoretic interpretation of constructive domain theory ⋮ Game semantics of Martin-Löf type theory ⋮ The paradox of trees in type theory ⋮ Remarks on Martin-Löf's partial type theory ⋮ Hyperfinite type structures ⋮ An adequacy theorem for dependent type theory ⋮ Concrete models of computation for topological algebras ⋮ Well-ordering proofs for Martin-Löf type theory ⋮ European Summer Meeting of the Association for Symbolic Logic, Uppsala 1991 ⋮ Computational foundations of basic recursive function theory ⋮ A natural semantics of first-order type dependency

Cites Work

• On the syntax of Martin-Löf's type theories
• LCF considered as a programming language
• Domain theoretic models of polymorphism
• Constructive mathematics and computer programming
• Recursive models for constructive set theories
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Precision of double sampling estimators for comparing two probabilities
• The Category-Theoretic Solution of Recursive Domain Equations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item