Proofs for "Constructive Galois Connections" by Darais et al.
592
Proofs for the ICFP'16 paper "Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory" by David Darais and David Van Horn.
Note that I made minor changes to upgrade the official repo to Agda 2.6.1
I could not get the official repo to typecheck with 2.5.3 within reasonable time. Also, typechecking doesn't terminate with Agda version 2.6.2.*. Hence, I used 2.6.1.
docker run -it --rm sourcedennis/cgc make
docker run -it --rm -v "$PWD/html:/proofs/html" sourcedennis/cgc /bin/bash -c "agda --html --html-dir=html CDGAI.agda; agda --html --html-dir=html AGT.agda"
This image was built on top of my Agda Docker image sourcedennis/agda-mini:2.6.1.
Content type
Image
Digest
sha256:8264e1313…
Size
49.4 MB
Last updated
about 4 years ago
docker pull sourcedennis/cgc