Prawf: An Interactive Proof System for Program Extraction

We present an interactive proof system dedicated to program extraction from proofs. In a previous paper [5] the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundness proven. The present contribution describes a prototype implementation and explains its use through...

Descripción completa

Detalles Bibliográficos
Autores principales: Berger, Ulrich, Petrovska, Olga, Tsuiki, Hideki
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7309514/
http://dx.doi.org/10.1007/978-3-030-51466-2_12
Descripción
Sumario:We present an interactive proof system dedicated to program extraction from proofs. In a previous paper [5] the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundness proven. The present contribution describes a prototype implementation and explains its use through several case studies. The system benefits from an improvement of the theory which makes it possible to extract programs from proofs using unrestricted strictly positive inductive and coinductive definitions, thus removing the previous admissibility restrictions.

Ejemplares similares