Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22944-2_29 | CALCO |
Keywords | Field | DocType |
algebraic proof,exact real number,efficient program,proof-theoretic method,computational content,interactive system,program extraction,digit representation | Initial algebra,Discrete mathematics,Programming language,Algebraic number,Interactive proof system,Computer science,Theoretical computer science,Exploit,Mathematical proof,Signed-digit representation,Parsing,Real number | Conference |
Citations | PageRank | References |
8 | 0.59 | 18 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ulrich Berger | 1 | 95 | 16.16 |
| Kenji Miyamoto | 2 | 8 | 0.59 |
| Helmut Schwichtenberg | 3 | 373 | 44.83 |
| Monika Seisenberger | 4 | 61 | 7.26 |