Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Recurso digital |
| Language: | |
| Published: |
Zenodo
2025
|
| Subjects: | |
| Online Access: | https://doi.org/10.5281/zenodo.14917573 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of 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>