Completeness, minimal logic and programs extraction
| Autor: | Christophe Raffalli |
|---|---|
| Rok vydání: | 2001 |
| Předmět: |
Program extraction
Discrete mathematics Model theory Correctness General Computer Science λ-calculus Intuitionistic logic Original proof of Gödel's completeness theorem Intuitionnistic Logic Theoretical Computer Science TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES AF2-type system Minimal logic Types Computer Science::Programming Languages Kripke semantics Gödel's completeness theorem Completeness (statistics) Computer Science(all) Mathematics |
| Zdroj: | Theoretical Computer Science. 254:259-271 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/s0304-3975(99)00141-3 |
| Popis: | We formalize, in the AF 2 -type system, a completeness and correctness theorem for a modified Kripke semantics for minimal logic. We show that any program extracted from a proof of the completeness theorem translates higher-order encoding of a λ -term into a Debruijn encoding of another λ -term with the same type. We also show that any program extracted from the correctness theorem performs the reverse translation. Moreover, in both cases, there is one proof which corresponds to a program that does not change the underlying λ -term. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect