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
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
- Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika: Extracting verified decision procedures: DPLL and resolution (2015)
- Miyamoto, Kenji; Schwichtenberg, Helmut: Program extraction in exact real arithmetic (2015)
- Berger, Ulrich; Seisenberger, Monika; Woods, Gregory J.M.: Extracting imperative programs from proofs: In-place Quicksort (2014)
- Miyamoto, Kenji; Nordvall Forsberg, Fredrik; Schwichtenberg, Helmut: Program extraction from nested definitions (2013)
- Lawrence, Andrew; Berger, Ulrich; Seisenberger, Monika: Extracting a DPLL algorithm (2012)
- Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut; Seisenberger, Monika: Minlog -- a tool for program extraction supporting algebras and coalgebras (2011)
- Berger, Ulrich; Seisenberger, Monika: Proofs, programs, processes (2010)
- Wiedijk, Freek (ed.): The seventeen provers of the world. Foreword by Dana S. Scott.. (2005)