Program extraction from nested definitions

DOI10.1007/978-3-642-39634-2_27MaRDI QIDQ5327357zbMATH OpenOpenAlexFDO

Authors Kenji Miyamoto, Fredrik Nordvall Forsberg, Helmut Schwichtenberg

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_27

Mathematics Subject Classification ID

Recommendations

• Minlog -- a tool for program extraction supporting algebras and coalgebras
• Program extraction from normalization proofs
• Program extraction in exact real arithmetic
• Extraction and verification of programs by analysis of formal proofs
• Program extraction via typed realisability for induction and coinduction

Cited in

(8)

• Program extraction for mutable arrays
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• A realizability interpretation of Church's simple theory of types
• Nonflatness and totality
• Program extraction applied to monadic parsing
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
• Verified program extraction in number theory: the fundamental theorem of arithmetic and relatives

Describes a project that uses

Uses Software

• Haskell
• Minlog

This page was built for publication: Program extraction from nested definitions

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