Resumen:
MetaCoq is a library designed to explore the theory and implementation of Coq itself, within Coq. It consists of four main components. The first, Template-Coq, is a reification of terms and environments handled by Coq’s core (in OCaml), enabling direct interaction with the system by developing metaprograms using the Gallina language and a monad representing Coq’s kernel interface. The second component, PCUIC, formalizes a variant of the type system of the Calculus of Inductive Constructions and its essential metatheoretical properties, ensuring the correctness of the system and facilitating the study of possible extensions. The third component is a certified version of a type and environment checker for this calculus, guaranteeing the decidability, soundness, and completeness of type inference according to PCUIC’s specification. Lastly, the fourth component is a certified development of the procedure for erasing proofs and types from PCUIC into a pure lambda calculus, forming the core of Coq’s extraction mechanism, enabling the safe extraction of the type checker into executable languages. In this talk, I will provide an overview of these four components and their applications in producing certified programs in Coq with the highest safety guarantees.

--
Comunicaciones DCC