Not signed in (Sign In)

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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.


Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)