Authors: Catherine Dubois, Nicolas Magaud and Alain Giorgetti
This repository distributes a framework for dealing with different data representations, with partial automation in proving that these different representations are isomorphic. The representations and the corresponding transformations are implemented in Coq. In addition, the Coq QuickChick plugin is used to implement random generators for the different representations. The methodology, presented in [DMG23], is illustrated with its application to data related to families of lambda terms.
[DMG23] C. Dubois, N. Magaud, and A. Giorgetti. Pragmatic isomorphism proofs between Coq representations: application to lambda-term families. Accepted for publication. 2023.
The code is known to work at least from Coq 8.10.2 (with QuickChick 1.2.1) to Coq 8.16.1 (with QuickChick 1.6.4).
Coq and the Coq plugin QuickChick are assumed to be installed.
Run the case study as follows:
cd src
make
https://github.com/alaingiorgetti/postTYPES2022
This program is distributed under the GNU GPL 3. See the enclosed LICENSE file.