No Cover Image

Conference Paper/Proceeding/Abstract 577 views

Prawf: An Interactive Proof System for Program Extraction

Ulrich Berger Orcid Logo, Olga Petrovska, Hideki Tsuiki

Lecture Notes in Computer Science, Volume: 12098, Pages: 137 - 148

Swansea University Author: Ulrich Berger Orcid Logo

Full text not available from this repository: check for access using links below.

Abstract

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

Full description

Published in: Lecture Notes in Computer Science
ISSN: 0302-9743 1611-3349
Published: Cham Springer International Publishing 2020
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa57995
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: We present an interactive proof system dedicated to program extraction from proofs. In a previous paper the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundnessproven. 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.
College: Faculty of Science and Engineering
Start Page: 137
End Page: 148