Foundations of Functional Programming/UTT-Σ

Foundations of Functional Programming/UTT-Σ is a stub. Learn how you can help Wikiversity to expand it.

UTT_Σ is a fairly elaborate explicitly typed λ-calculus. It can be viewed as an extension of the calculus of constructions (λPω) of the λ-cube, which is the fullest-featured system of the λ-cube, featuring dependent types, polymorphic types, and type constructors. UTT_Σ was introduced by Ulf Norell in his PhD thesis (Norell 2007), and it is the basic type theory underlying the Agda programming language.

UTT_Σ differs from the calculus of constructions in three primary ways.

Rather than including just two sorts $\text{Type}_0$ and $\text{Type}_1$ , it includes an infinite hierarchy of sorts, $\text{Type}_0, \text{Type}_1, \text{Type}_2, ...$ .
Its sorts are cumulative, meaning that when $n \leq m$ , any type belonging to $\text{Type}_n$ also belongs to $\text{Type}_m$ . This fact means that types are not unique up to β-conversion, and necessitates the introduction of a subtyping relation.
It includes a wider variety of types than the calculus of constructions. It includes dependent pair types and a unit type in addition to sorts and dependent function types. The additional types are interesting primarily because of their interpretation under the Curry-Howard correspondence.

This article is issued from Wikiversity - version of the Thursday, September 24, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.