HOcore

The long version of the paper presented at ITP 2015, including with the appendix and links to the Coq definitions, can be found here.

The development, as well as the sources of the paper, can be downloaded here. See the README file for more information.

Preliminary results have been presented at JFLA 2012 (in French) and JFLA 2015.

The html version of the development can be found here.

Contacts:

• Alan Schmitt (project leader)
• Martín Escarrá
• Petar Maksimović

The long version of Lionel Zoubritzky's report is here.

The source code for the following is available:

• the interpreter;
• the abstract machine in OCaml;
• the abstract machine in HOcore.