In which we extend our Gradual Calculus of Inductive Constructions to internalize precision and allow for sound reasoning over gradual programs.
en ¦ fr > Publications
In which we investigate gradual variations on the Calculus of Inductive Construction. Presented at POPL '22.
In which I presents a bidirectional type system for the Calculus of Inductive Constructions.
Under Creative Commons CC0 License, source on github. Built using Pelican. Theme adapted from pelican-svbhack by Giulio Fidente.