Artifact of the paper 'Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation'
Fuente:
Zenodo
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Recurso digital |
| Pubblicazione: |
Zenodo
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866902148940300288 |
|---|---|
| author | Schuster, Philipp Müller, Marius Ostermann, Klaus Brachthäuser, Jonathan Immanuel |
| author_facet | Schuster, Philipp Müller, Marius Ostermann, Klaus Brachthäuser, Jonathan Immanuel |
| contents | <p>The artifact consists of</p> <ul> <li>an intrinsically-typed implementation in Idris 2 of the AxCut language and the abstract machine semantics, along with a simple parser, a type checker and code generation for aarch64, RISC-V and x86-64.</li> <li>an intrinsically-typed implementation in Idris 2 of the normalization procedure transforming standard linear sequent calculus terms into AxCut.</li> <li>the benchmarks conducted for the evaluation of the compilation approach. This repository contains the sources of the benchmark programs for all languages we have benchmarked against. There are descriptions of what each benchmark program does. For comparison, there are also two files containing results: <ul> <li><code>results-paper.md</code> contains the results for the largest input from the paper.</li> <li><code>results-example.md</code> contains the results for the largest input from a run of the benchmarks in the below Docker container on an Intel(R) Core(TM) i5-8265U.</li> </ul> </li> </ul> <p>This repository contains a <code>Dockerfile</code> which can be used to build a Docker image for a container with all necessary languages installed. Everything can be run inside this container.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_14917573 |
| institution | Zenodo |
| language | |
| publishDate | 2025 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Artifact of the paper 'Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation' Schuster, Philipp Müller, Marius Ostermann, Klaus Brachthäuser, Jonathan Immanuel compilers intermediate representations sequent calculus <p>The artifact consists of</p> <ul> <li>an intrinsically-typed implementation in Idris 2 of the AxCut language and the abstract machine semantics, along with a simple parser, a type checker and code generation for aarch64, RISC-V and x86-64.</li> <li>an intrinsically-typed implementation in Idris 2 of the normalization procedure transforming standard linear sequent calculus terms into AxCut.</li> <li>the benchmarks conducted for the evaluation of the compilation approach. This repository contains the sources of the benchmark programs for all languages we have benchmarked against. There are descriptions of what each benchmark program does. For comparison, there are also two files containing results: <ul> <li><code>results-paper.md</code> contains the results for the largest input from the paper.</li> <li><code>results-example.md</code> contains the results for the largest input from a run of the benchmarks in the below Docker container on an Intel(R) Core(TM) i5-8265U.</li> </ul> </li> </ul> <p>This repository contains a <code>Dockerfile</code> which can be used to build a Docker image for a container with all necessary languages installed. Everything can be run inside this container.</p> |
| title | Artifact of the paper 'Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation' |
| topic | compilers intermediate representations sequent calculus |
| url | https://doi.org/10.5281/zenodo.14917573 |