Guilhem Jaber, Forcing the Calculus of Construction to get Generalized Inductive Types
Schedule
- Feb. 14, 2012, 16:15 - 17:00
Abstract
(Joint work with N. Tabareau)
In this talk, I will present an extension of the Calculus of Construction (the theory behind Coq) which allows to extend modularly the type system with new constructors and new inference rules. The idea is to define a translation between the new system and the original one, following the idea of Krivine and Miquel to study the translation of proofs induced by forcing.
Here, our translation of forcing will in fact be an internalization in the type theory of the topos of presheaves of Birkedal et al.
I will then show how we can use this technique to allow negative occurence in the inductive types of Coq. Finally, if time permits, I will talk about how to use the forcing method to extend the type system with “non-constructive” objects.
Attachments
(Joint work with N. Tabareau)
In this talk, I will present an extension of the Calculus of Construction (the theory behind Coq) which allows to extend modularly the type system with new constructors and new inference rules. The idea is to define a translation between the new system and the original one, following the idea of Krivine and Miquel to study the translation of proofs induced by forcing. Here, our translation of forcing will in fact be an internalization in the type theory of the topos of presheaves of Birkedal et al.
I will then show how we can use this technique to allow negative occurence in the inductive types of Coq. Finally, if time permits, I will talk about how to use the forcing method to extend the type system with “non-constructive” objects.