Program extraction from nested definitions
Miyamoto, Kenji and Nordvall Forsberg, Fredrik and Schwichtenberg, Helmut (2013) Program extraction from nested definitions. In: Interactive Theorem Proving. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, Berlin, pp. 370-385. ISBN 9783642396335
Full text not available in this repository.Request a copy from the Strathclyde authorAbstract
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.
| Author(s): | Miyamoto, Kenji, Nordvall Forsberg, Fredrik and Schwichtenberg, Helmut | Item type: | Book Section |
|---|---|
| ID code: | 53121 |
| Keywords: | coinduction, computational contents, formalisation, Haskell programs, program extraction, proof assistant, uniformly continuous, Electronic computers. Computer science, Artificial Intelligence |
| Subjects: | Science > Mathematics > Electronic computers. Computer science |
| Department: | Faculty of Science > Computer and Information Sciences |
| Depositing user: | Pure Administrator |
| Date deposited: | 28 May 2015 11:13 |
| Last modified: | 01 Feb 2019 03:34 |
| Related URLs: | |
| URI: | https://strathprints.strath.ac.uk/id/eprint/53121 |
| Export data: |
CORE (COnnecting REpositories)
CORE (COnnecting REpositories)