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
_version_ 1783549222805569536
author Berger, Ulrich
Petrovska, Olga
Tsuiki, Hideki
author_facet Berger, Ulrich
Petrovska, Olga
Tsuiki, Hideki
author_sort Berger, Ulrich
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7309514
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73095142020-06-23 Prawf: An Interactive Proof System for Program Extraction Berger, Ulrich Petrovska, Olga Tsuiki, Hideki Beyond the Horizon of Computability Article 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. 2020-06-24 /pmc/articles/PMC7309514/ http://dx.doi.org/10.1007/978-3-030-51466-2_12 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Berger, Ulrich
Petrovska, Olga
Tsuiki, Hideki
Prawf: An Interactive Proof System for Program Extraction
title Prawf: An Interactive Proof System for Program Extraction
title_full Prawf: An Interactive Proof System for Program Extraction
title_fullStr Prawf: An Interactive Proof System for Program Extraction
title_full_unstemmed Prawf: An Interactive Proof System for Program Extraction
title_short Prawf: An Interactive Proof System for Program Extraction
title_sort prawf: an interactive proof system for program extraction
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7309514/
http://dx.doi.org/10.1007/978-3-030-51466-2_12
work_keys_str_mv AT bergerulrich prawfaninteractiveproofsystemforprogramextraction
AT petrovskaolga prawfaninteractiveproofsystemforprogramextraction
AT tsuikihideki prawfaninteractiveproofsystemforprogramextraction

Ejemplares similares