University of Birmingham > Talks@bham > Lab Lunch > A Brouwerian Intuitionistic Type Theory (Part 3)

## A Brouwerian Intuitionistic Type Theory (Part 3)Add to your list(s) Download to your calendar using vCal - Vincent Rahli (University of Birmingham)
- Thursday 10 October 2019, 12:00-13:00
- CS 217.
If you have a question about this talk, please contact Todd Waugh Ambridge. Please contact Todd if you wish to give a talk this term! This is the concluding part of Vincent’s talk. In this talk I will present recent additions we made to CTT —-the logic implemented by the Nuprl proof assistant—-in order to turn it into a Brouwerian Intuitionistic Type Theory. Namely, we added Brouwer’s continuity principle for numbers as well as his bar induction principle—-from which we get W types. Using our implementation or CTT in Coq, we made sure that these principles are consistent with Nuprl by proving that they are valid w.r.t. Nuprl’s semantics. In order to validate these principles we added named exceptions as well choice sequences to Nuprl’s computation system. We initially only added choice sequences to CTT ’s metatheory as an instrumental tool to derive Bar Induction, and not to the theory itself. However, Brouwer originally introduced choice sequences as first class citizens in his logic. Therefore, in our pursuit of a Brouwerian Intuitionistic Type Theory, we have recently added choice sequences to Nuprl’s theory, and have proved that the resulting theory satisfies several of the standard choice sequence axioms. I will conclude with a discussion of positive and negative results we derived from these constructs/principles: among other things regarding the law of excluded middle, the axiom of choice, Markov’s principle, and Kripke’s schema. This is joint work with Liron Cohen (Ben-Gurion University, Israel), and Mark Bickford & Bob Constable (Cornell University, USA ). 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 listsNanoscale Physics Seminars Centre for Systems Biology Coffee Mornings Condensed Matter Physics Seminars## Other talksTBC |