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

DOI10.1007/978-3-030-51466-2_12OpenAlexW3037147088MaRDI QIDQ2106598FDOQ2106598

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

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

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

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

Cited In (2)

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

Uses Software

• Coq
• Isabelle
• Nuprl
• 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)