-
Notifications
You must be signed in to change notification settings - Fork 19
UPenn Coq Working Group
Here live the materials for the 2022 UPenn Coq Working Group.
- Topic: Equations and Locally Nameless
- Leader: Stephanie
- Location/Time: Levine 307, 12-2pm, also on Zoom
Original locally nameless representation tutorial: https://github.com/DeepSpec/dsss17/tree/master/Stlc
- Topic: Coinduction Library
- Leader: Yannick
- Location/Time: Levine 307, 12-2pm, also on Zoom
The purpose of this session is to discover the
coinductionlibrary, written by Damien Pous. My plan is to go with everyone through basic notions of coinduction and proofs by coinduction in lattices on paper, and to see how it can be mirrored in Coq using the library. We will then discuss something called up-to techniques, and once again study what they look like using the library.
We will study, depending on time and interest, streams and/or CCS as examples. We’ll use files with holes to be filled live, so please be ready to prove things :) But of course no need to stick to the plan, feel free to derail it and ask questions/offer comments during the session!
The library is based on the paper
Coinduction All the Way Upby Damien Pous (https://hal.archives-ouvertes.fr/hal-01259622).
Most of the material we will use has been initially written by Damien as well, and can be found on github (https://github.com/damien-pous/coinduction-examples)! We will use modified versions of these files containing exercices to fill in.
Installation pre-requisites:
opam install coq-coinduction(Support for 8.15 is now available on opam as well)- If we cover ccs, then additional useful dependencies:
opam install coq-aac-tacticsopam install coq-relation-algebra
Homework: If you have never studied anything related to bisimulation or coinduction, it would be great if you find the time to just read the chapter 1 (p11 to p27) of Davide Sangiorgi’s book
Introduction to Bisimulation and Coinduction(pm me if you need a pdf version of it).