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

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

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

Martin-Löf type theory; consistently complete algebraic cpo's; effective continuous function; effective continuous functor; effective domain; operational semantics of type theory; partial type theory

Mathematics Subject Classification ID

68Q55: Semantics in the theory of computing

06B35: Continuous lattices and posets, applications

03F35: Second- and higher-order arithmetic and fragments

03F50: Metamathematics of constructive systems

03D45: Theory of numerations, effectively presented structures

Related Items

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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