Domain interpretations of Martin-Löf's partial type theory
type: Item
instance of: scholarly article
title: Domain interpretations of Martin-Löf's partial type theory
zbMATH Open document ID: 0704.03041
DOI: 10.1016/0168-0072(90)90044-3
author: Erik Palmgren
author: Viggo Stoltenberg-Hansen
published in: Annals of Pure and Applied Logic
publication date: 1990-01-01T00:00:00Z
review text: The Martin-Löf type theory considered is a monomorphic version, i.e. all type information is included in the terms, with the intensional identity type and containing a fixed point operator but not containing universes. On the domain side, the category DOM is considered, consisting of consistently complete algebraic cpo's with projection pairs as morphisms or, rather, effective such in terms of recursive enumeration theory. Each context \(\Gamma\) is interpreted as an effective domain \(\Gamma\), each (dependent) type A in the context \(\Gamma\) is interpreted as an effective continuous functor \(A_{\Gamma}: \Gamma\to DOM\) and each element \(a\in A\) in the context \(\Gamma\) is interpreted as an effective continuous function \(a_{\Gamma}\) over \(A_{\Gamma}\). Equality is interpreted as set theoretic equality. Two interpretations are given, one of which is shown to be adequate for the operational semantics of type theory in the sense that a closed term a terminates iff \(a=\perp\). The interpretation has been modified and extended to type theory including universes in another paper of the first author [A domain interpretation of Martin-Löf's partial type theory with one universe, U.U.D.M. Report (1989)].
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 03D45
Mathematics Subject Classification ID: 06B35
zbMATH DE Number: 4154442
zbMATH Keywords: partial type theory
zbMATH Keywords: Martin-Löf type theory
zbMATH Keywords: consistently complete algebraic cpo's
zbMATH Keywords: effective domain
zbMATH Keywords: effective continuous functor
zbMATH Keywords: effective continuous function
zbMATH Keywords: operational semantics of type theory
MaRDI profile type: Publication
full work available at URL: 0168-0072(90)90044-3
OpenAlex ID: W2067618205
cites work: Recursive models for constructive set theories
cites work: Q3787462
cites work: Domain theoretic models of polymorphism
cites work: Constructive mathematics and computer programming
cites work: Q3999860
cites work: Precision of double sampling estimators for comparing two probabilities
cites work: LCF considered as a programming language
cites work: Q3768897
cites work: Q3664454
cites work: An interpretation of Martin-Löf's type theory in a type-free theory of propositions
cites work: The Category-Theoretic Solution of Recursive Domain Equations
cites work: On the syntax of Martin-Löf's type theories
Recommended article: Remarks on Martin-Löf's partial type theory
Recommended article: A type theoretic interpretation of constructive domain theory
Recommended article: Q3322097
Recommended article: Q4247302
Recommended article: On the syntax of Martin-Löf's type theories
Recommended article: An interpretation of Martin-Löf's type theory in a type-free theory of propositions
Recommended article: An information system interpretation of Martin-Löf's partial type theory with universes
Recommended article: Kripke Semantics for Martin-Löf’s Extensional Type Theory
Recommended article: Kripke Semantics for Martin-L\"of's Extensional Type Theory
Recommended article: Characterizing the interpretation of set theory in Martin-Löf type theory
description: scientific article; zbMATH DE number 4154442