## Reconstructing Observational Type TheoryAdd to your list(s) Download to your calendar using vCal - Neel Krishnaswami (University of Birmingham)
- Thursday 10 July 2014, 14:00-15:00
- CS 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 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 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. ## This talk is included in these lists:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsComputer Science Lunch Time Talk Series Facts and Snacks Human Computer Interaction seminars## Other talksTBC |