Fellowship Prover

These are the sources for the Fellowship prover written by Florent Kirchner and Claudio Sacerdoti Coen. The prover is an implementation of the $\bar{\lambda}\mu\tilde{\mu}$-calculus due to Pierre-Louis Curien and Hugo Herbelin. The system and the theory behind it is described extensively in Florent Kirchner's PhD-thesis.

Setup

Clone the directory to a destination of your choosing. Navigate to one of the available versions in the tags subdirectory, e.g. 'fellowship-0.1.0'. Use 'make' to build (requires OCaml). As of late 2024, the system still works on Linux (tested on WSL) and MacOS

Usage

Use ./fsp to run the prover. Use 'help.' to get help. For further questions refer to Florent Kirchner's PhD-thesis, especially chapter 7. The tests folder contains some examples to run.

License

This repository carries two licenses, scoped to different parts of the tree:

• The Fellowship source under fsp/ is distributed under its original license, the CeCILL v2.0, by Florent Kirchner and Claudio Sacerdoti Coen. See fsp/trunk/COPYING for the full text; it is unchanged from upstream.
• Museum-specific material added for this rehosting (this README and other files outside fsp/) is licensed under GPLv3, per the top-level LICENSE file.

CeCILL v2.0 explicitly permits combination with GPL-covered code (Article 5.3.4), so the two licenses coexist without conflict; they simply cover different parts of the repository.