HOcore in Coq

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.


Abstract machine for HOcore

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

The source code for the following is available: