Computer Science Seminar Series

Abstract

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 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 semantics. In order to validate these principles we added named exceptions as well choice sequences to Nuprl's computation system. I will conclude with a discussion of positive and negative results we derived from these 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 Mark Bickford and Bob Constable from Cornell.
http://www.nuprl.org/html/Nuprl2Coq/bar-induction-lics-short.pdf

Bio

Vincent Rahli received a PhD in computer science from Heriot-Watt University in 2011, on the theory and applications of intersection type systems. From 2011 to 2015 he was a research associate at Cornell University where he worked in the PRL group led by Prof. Robert L. Constable, discovering and perfecting mathematically sound programming tools such as proof assistants for building highly trustworthy systems. Since 2015 he has been a member of the CritiX research group at the University of Luxembourg, led by Prof. Paulo Verissimo. His research interests include programming languages, type theory, distributed systems, and proof assistants.

Website: http://wwwfr.uni.lu/snt/people/vincent_rahli

Hosts: Fairouz Kamareddine and Joe Wells

• Back to list