CONTENTS OF THIS FILE
---------------------
 * Introduction
 * Requirements
 * Installation
 * Support


INTRODUCTION
------------

The 'HOCore in Coq' project consists of a set of definitions and proofs
of HOCore: A minimal higher-order process calculus, formalized in
Coq: The Proof Assistant.

* For a full description of 'HOCore in Coq', read the article found in the
documentation or visit the project page:

    http://www.irisa.fr/celtique/aschmitt/research/hocore/

REQUIREMENTS
------------

* For compiling the core of proofs:

    - coq 8.4pl2 or higher (http://coq.inria.fr/download)

* For producing the article pdf:

    - tex live 2010 or higher (https://www.tug.org/texlive/)
    - emacs 24 or higher (http://www.gnu.org/software/emacs/)
    - org-mode 8.0 or higher (http://orgmode.org/elpa.html)
      note that if you use emacs 25 or higher, the included version of
      org-mode is sufficient
    - pygments 1.6 or higher (http://pygments.org/download/)


INSTALLATION
------------

* All coq files (.v) are compiled in the coq directory with:

    ./fetch_tlc
    make -C tlc
    make all

* Compiling the article about 'HOCore in Coq' in the paper directory:

    Make sure org-mode is correctly installed in Emacs. We highly recommend to
    install org-mode from Emacs Lisp Package Archive (ELPA) following the
    instructions found in the link in the requirements. Afterwards, you must
    edit the file 'local-settings.el' to point to your org installation. See
    that file for further instructions.
    
    To generate the pdf, the default key binding is:

        C-c C-e l p

    You can also use the following make commands to generate the printed
    version
    
        make HOCore_ITP_final.pdf

    and the online version with links and the appendix

        make HOCore_ITP.pdf

SUPPORT
-------

To submit bug reports or any questions regarding the project. Please
contact:

    alan.schmitt@inria.fr (Alan Schmitt, project leader)
    mescarra@gmail.com (Martín Escarrá)
    petar.maksimovic@inria.fr (Petar Maksimović)