Name
Abstract | ||
|---|---|---|
Minlog is a proof assistant which automatically extracts computational content in an extension of Gödel's T from formalized proofs. We report on extending Minlog to deal with predicates defined using a particular combination of induction and coinduction, via so-called nested definitions. In order to increase the efficiency of the extracted programs, we have also implemented a feature to translate terms into Haskell programs. To illustrate our theory and implementation, a formalisation of a theory of uniformly continuous functions due to Berger is presented. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-39634-2_27 | ITP |
Keywords | Field | DocType |
proof assistant,extracts computational content,so-called nested definition,program extraction,continuous function,particular combination,haskell program,formalized proof | Programming language,Gödel,Computer science,Algorithm,Theoretical computer science,Mathematical proof,Coinduction,Uniform continuity,Haskell,Predicate (grammar),Stream processing,Proof assistant | Conference |
Volume | ISSN | Citations |
7998 | 0302-9743 | 1 |
PageRank | References | Authors |
0.35 | 17 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kenji Miyamoto | 1 | 2 | 0.72 |
| Fredrik Nordvall Forsberg | 2 | 28 | 8.82 |
| Helmut Schwichtenberg | 3 | 373 | 44.83 |