\textsc{Prawf}: an interactive proof system for program extraction

DOI10.1007/978-3-030-51466-2_12MaRDI QIDQ2106598zbMATH OpenOpenAlexFDO

Authors Ulrich Berger, Olga Petrovska, Hideki Tsuiki

Publication date 16 December 2022

Full work available at URL https://doi.org/10.1007/978-3-030-51466-2_12

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• scientific article; zbMATH DE number 2003148
• Proofs and programs: A naïve approach to program extraction
• Extraction and verification of programs by analysis of formal proofs
• Proofs, programs, processes
• scientific article; zbMATH DE number 2003158

Cites work

• scientific article; zbMATH DE number 2061716 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Intuitionistic fixed point logic
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• Optimized program extraction for induction and coinduction
• Real number computation through Gray code embedding.
• Realisability for induction and coinduction with applications to constructive analysis

Cited in

(2)

• Intuitionistic fixed point logic
• Extracting total Amb programs from proofs

Describes a project that uses

Uses Software

• Isabelle
• Nuprl
• Coq
• Minlog

This page was built for publication: \textsc{Prawf}: an interactive proof system for program extraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2106598)