Achievements and Planned Activities
Ongoing research
-
Hybrid and gradual verification in proof assistants
Study the foundations of hybrid and gradual verifications in proof assistants to allow smoothly combining static and dynamic verification in an expressive setting.
-
Gradual Indexed Inductive Types
Extending the Gradual Calculus of Inductive Constructions (GCIC) with support for indexed inductive types and implementing a prototype in Coq.
-
Internal reasoning about precision and graduality in proof assistants
Study and further develop the ideas of internalizing precision and graduality, extending them to other gradual variants of the CIC, in order to demonstrate its benefits.
Publications
-
Proceedings of the ACM on Programming Languages, volume 8, number ICFP, pp.255:1-255:29, August 2024, ACM Press
Talks
-
Nicolas Tabareau - Department of Computer Science, Universidad de Chile - November 28, 2024
-
Kenji Maillard - ICFP 2024 - September 03, 2024
-
Nicolas Tabareau - Department of Computer Science, Universidad de Chile - December 06, 2023
-
Mara Malewski - FunLep 2023 - May 19, 2023
-
Éric Tanter - FunLep 2023 - May 18, 2023
-
Nicolas Tabareau - Department of Computer Science, Universidad de Chile - March 14, 2023
Code
-
A prototype implementation of GCIC written in OCaml.
-
GRIP prototype implementation in Coq
A prototype implementation of the cast-calculus for GCIC (GRIP) written in Coq itself, using different extension mechanisms.
Prior related joint work
-
Proceedings of the ACM on Programming Languages, volume 6, number ICFP, pp.931-959, August 2022, ACM Press
-
ACM Transactions on Programming Languages and Systems, volume 44, number 2, June 2022 Presented at POPL 2022
-
Journal of the ACM, volume 68, number 1, pp.5:1-5:44, January 2021, ACM Press
-
Proceedings of the ACM on Programming Languages, volume 3, number ICFP, pp.108:1-108:29, August 2019, ACM Press
-
Proceedings of the ACM on Programming Languages, volume 2, number ICFP, pp.92:1-92:29, September 2018, ACM Press Distinguished Paper Award - superseded by JACM article "The Marriage of Univalence and Parametricity" (2021)
-
Journal of Functional Programming, volume 28, pp.9:1-9:44, 2018, Cambridge University Press
-
Proceedings of the 21st ACM SIGPLAN Conference on Functional Programming (ICFP 2016), pp.298-310, Nara, Japan, September 2016, ACM Press
-
Proceedings of the 11th ACM Dynamic Languages Symposium (DLS 2015), pp.26-40, Pittsburgh, PA, USA, October 2015, ACM Press