Skip to content
/ velo-lang Public

Velo is a tiny language (STLC + Hutton's Razor with Bools) to showcase & explore efficient verified implementations in Idris2.

License

Notifications You must be signed in to change notification settings

jfdm/velo-lang

Repository files navigation

Velo.

Build Status

A tiny language to explore efficient verified implementations of functional languages in Idris2.

Artefact

We also include scripts to generate a reproducible artefact.

Please consult the following project to generate the base virtual box image required, and how we approach the building of the artefact.

https://github.com/jfdm/packer-idris

You will also need to have working installations of Katla to facilitate source code highlighting.

Once you have generated the image you can generate the artefact as follows:

SOURCE_VM="<location of the base ovf>" make artefact

This will generate in artefact the following files:

  1. velo.box :: A Virtual Box virtual machine that contains Velo's source code & test suite;
  2. velo.tar.gz :: A copy of Velo's source code, and generated IdrisDoc;
  3. velo_doc.tar.gz :: A copy of the IdrisDoc for the coding project;
  4. velo_html.tar.gz :: A copy of the katla generated html showing semantically highlighted code;
  5. velo.pdf :: A copy of the submitted paper;

About

Velo is a tiny language (STLC + Hutton's Razor with Bools) to showcase & explore efficient verified implementations in Idris2.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Languages