Keyword:Calculus of Inductive Constructions

Publications
A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions Pierre Corbineau, Basile Gros and Jean-Francois Monin In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Aligning HOL-Light and Rocq Libraries Formally Frédéric Blanqui and Antoine Gontard In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning