# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJan 12th 2014
• (edited Jan 12th 2014)

Is this here an accurate description of what is meant by the words “computational type theory”:

The term computational type theory is often used generally for intuitionistic type theory, referring to its computational content in view of the propositions-as-types and proofs-as-programs interpretation (e.g. Scholarpedia). More specifically it is used for type theory with inductive types and even more specifically (Fairtlough-Mendler 02) for modal type theory, hence for type theory equipped with a monad (in computer science) which exhibits a kind of computation.

?

• CommentRowNumber2.
• CommentAuthorspitters
• CommentTimeJan 13th 2014

It seems to be the dialect of MLTT used for NuPrl (Cornell).

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJan 13th 2014

This seems to be one of three meanings in which the term is used. I have now expanded in the entry as follows:

The term computational type theory has been used

1. generally for intuitionistic type theory in view of its computational content via the propositions-as-types and proofs-as-programs interpretation (e.g. Constable 02, Scholarpedia).

2. more specifically for intuitionistic type theory with inductive types and here specifically for the dialect of the language which is implemented in the NuPRL software (Constable et al. 86, NuPRL 05);

Constable, p. 6: $[$computational type theory$]$ considerably extended Per Martin-Löf’s Intuitionistic Type Theory (ITT) adding set types, quotient types, recursive types, partial object types (bar types)

As such computational type theory is similar to the calculus of inductive constructions.

3. for modal type theory, specifically for type theory equipped with a monad (in computer science) that preserves finite products, which exhibits a kind of computation (Benton-Bierman-de Paiva 93, Fairtlough-Mendler 02).

The internal logic of computational type theory in this sense is also called propositional lax logic (Fairtlough-Mendler 97, Crolard) or computational logic.