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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element