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

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

Olga Petrovska, Ulrich Berger, 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)

Related Items (2)

Extracting total Amb programs from proofs ⋮ Intuitionistic fixed point logic

Uses Software

• Unnamed Item
• Unnamed Item
• Nuprl
• Minlog

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Real number computation through Gray code embedding.
• Optimized program extraction for induction and coinduction
• Intuitionistic fixed point logic
• Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras

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