×

Minlog

swMATH ID: 9765
Software Authors: Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut; Seisenberger, Monika
Description: Minlog – a tool for program extraction supporting algebras and coalgebras. Minlog is an interactive system which implements proof-theoretic methods and applies them to verification and program extraction. We give an overview of Minlog and demonstrate how it can be used to exploit the computational content in (co)algebraic proofs and to develop correct and efficient programs. We illustrate this by means of two examples: one about parsing, the other about exact real numbers in signed digit representation.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-22944-2_29
Related Software: Coq; Nuprl; Isabelle; Agda; Isabelle/HOL; Haskell; Leo-III; Theorema; Satallax; PVS; Sledgehammer; Chaff; Metis_; LEGO; Isabelle/Isar; Archive Formal Proofs; cubicaltt; Pesca; Z; APS-1
Referenced in: 21 Publications

Referencing Publications by Year