Nicolas Tabareau

Partial type equivalences for verified dependent interoperability

2016 · ACM SIGPLAN Notices

Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading …

The fire triangle: how to mix substitution, dependent elimination, and effects

2019 · Proceedings of the ACM on Programming Languages

There is a critical tension between substitution, dependent elimination and effects in type theory. In this paper, we crystallize this tension in the form of a no-go theorem that constitutes the fire triangle of type …

Gradualizing the Calculus of Inductive Constructions

2020 · INRIA a CCSD electronic archive server

Acknowledging the ordeal of a fully formal development in a proof assistant such as Coq, we investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We …