Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality
type: Item
instance of: scholarly article
title: Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality
zbMATH Open document ID: 0945.03089
author: Geir Waagbø
published in: Archive for Mathematical Logic
publication date: 2000-09-27T00:00:00Z
review text: An interpretation of Martin-Löf type theory is given which consists of a domain \(D\), a subdomain (of infinitary type expressions) \(S\) of \(D\) and a continuous map \(I\) sending elements of \(S\) to subdomains of \(D\) thus providing meaning for the elements of types. These data are all obtained as least fixpoints of appropriate domain equations. Thereafter, a totality predicate is defined on \(S\) and on each \(I(s)\) in such a way that all denotable elements are in fact total and the empty type has no total elements. This provides a domain-theoretic model of Martin-Löf type theory which is still faithful w.r.t.\ its logical interpretation. As applications some nonderivability results are given, most importantly the nonderivability of the statement that all type 2 functionals are continuous. The latter result is somewhat remarkable since the model does interpret functions as continuous maps. One should mention that in the meantime this line of work has been considerably advanced by \textit{U. Berger} [``Continuous functionals of dependent and transfinite types'', in: S. B. Cooper et al. (eds.), Models and computability. Invited papers from the Logic Colloquium '97, Leeds, UK, Lond. Math. Soc. Lect. Note Ser. 259, 1-22 (1999)] who establishes a Kleene-Kreisel style density theorem for total maps for a similar interpretation of Martin-Löf's type theory.
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03D65
Mathematics Subject Classification ID: 03D45
zbMATH DE Number: 1275031
zbMATH Keywords: Martin-Löf type theory
zbMATH Keywords: domain theory
zbMATH Keywords: totality
zbMATH Keywords: fixpoints of domain equations
zbMATH Keywords: nonderivability results
zbMATH Keywords: type 2 functionals
MaRDI profile type: Publication
full work available at URL: s001530050114
OpenAlex ID: W1992193729
DOI: 10.1007/S001530050114
description: scientific article; zbMATH DE number 1275031