University of Birmingham > Talks@bham > Lab Lunch > Reconstructing Observational Type Theory

Reconstructing Observational Type Theory

Add to your list(s) Download to your calendar using vCal

  • UserNeel Krishnaswami (University of Birmingham)
  • ClockThursday 10 July 2014, 14:00-15:00
  • HouseCS 217.

If you have a question about this talk, please contact Neel Krishnaswami.

Observational type theory, originally introduced by Altenkirch and McBride, is a variant of dependent type theory in which propositional equality is extensional (i.e., supports function extensionality), but in which judgmental equality is intensional (i.e., does not contain the equality reflection rule).

This theory can be seen either as a fragment of homotopy type theory in which all types are sets, or a type theory embodying Bishop’s definition of a set as a set of rules for forming elements, together with a definition of an equality relation for those elements.

The chief virtue of OTT is that it supports both decidable typechecking, and also validates the “naive constructive” idea of equality—for example, function extensionality, quotients, and bisimulation implying equality for coinductive types are all allowable in OTT .

Despite its virtues, it has not seen much uptake. This is because its presentation relies on a nonstandard heterogenous equality, and its soundness is shown by a complex translation into extensional type theory.

In this talk, I’ll describe some in-progress work I’m doing which reformulates OTT in a simpler way, by (a) showing how equality elimination can be formulated as an inductive-recursive definition, and (b) giving a simple new account of proof irrelevance.

No theorems will be harmed (or produced) in the production of this talk. :)

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.