In which we extend our Gradual Calculus of Inductive Constructions to internalize precision and allow for sound reasoning over gradual programs.
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.