Reseña: Towards a formally verified proof assistant

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Towards a formally verified proof assistant.

Sus autores son Abhishek Anand y Vincent Rahli (de la Cornell University).

Su resumen es

This paper presents a formalization of Nuprl’s metatheory in Coq. It includes a nominal-style definition of the Nuprl language, its reduction rules, a coinductive computational equivalence, and a Curry-style type system where a type is defined as a Partial Equivalence Relation (PER) à la Allen. This type system includes Martin-Löf dependent types, a hierarchy of universes, inductive types and partial types. We then prove that the typehood rules of Nuprl are valid w.r.t. this PER semantics and hence reduce Nuprl’s consistency to Coq’s consistency.

El trabajo se presentará el lunes 14 de julio en el ITP 2014 (5th Conference on Interactive Theorem Proving).

El código de las correspondientes teorías en Coq se encuentra aquí.