Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2503.02975 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913800763998208 |
|---|---|
| author | Kappelmann, Kevin Huch, Fabian Stevens, Lukas Abdulaziz, Mohammad |
| author_facet | Kappelmann, Kevin Huch, Fabian Stevens, Lukas Abdulaziz, Mohammad |
| contents | We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that can simulate (and be simulated by) Turing Machines with a quadratic time and constant space blow-up. Our framework derives while-programs from functional programs written in a subset of Isabelle/HOL, namely tail-recursive functions with first-order arguments and algebraic datatypes. As far as we are aware, it is the first framework targeting a computation model that is reasonable in time and space from a complexity-theoretic perspective. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_02975 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model Kappelmann, Kevin Huch, Fabian Stevens, Lukas Abdulaziz, Mohammad Logic in Computer Science We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that can simulate (and be simulated by) Turing Machines with a quadratic time and constant space blow-up. Our framework derives while-programs from functional programs written in a subset of Isabelle/HOL, namely tail-recursive functions with first-order arguments and algebraic datatypes. As far as we are aware, it is the first framework targeting a computation model that is reasonable in time and space from a complexity-theoretic perspective. |
| title | Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2503.02975 |