Meven Lennon-Bertrand

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 …