“Certified Programming with Dependent Types” reading group @ iCIS
Upcoming and past talks
Year = 2016/2017
| Date and time | Topic/slides | Presenter | Location | Misc |
|---|---|---|---|---|
| Tuesday 22nd of November | Chapter 2: A quick example | Benoit Viguier | HG01.057 | |
| Wednesday 7th of December @ 14:45 ~ 15:45 | Chapter 3: Inductive Types | Dan Frumin | HG01.060 | coq-induct.v |
| Tuesday 7th of Mar @ 16:00 | Chapter 4: Inductive Predicates | Niels van der Weide | HG01.057 | Inductive Predicates.v, some notes |
| Tuesday 14th of Mar @ 16:00 | Chapter 5: Infinite data and proofs | Henning Basold | HG01.057 | coinduction tactic by Catalin Hritcu |
| Tuesday 28th of Mar @ 16:00 | Chapter 6: Subset Types and Variations | Guillaume Allais | HG01.057 | Subsetbase.v, Subsetpartial.v, Subsetdec.v, and Subsetmonadic.v |
| Tuesday 4th of Apr @ 16:00 | Chapter 7: General Recursion | Dan Frumin | HG02.028 | RecWf.v, RecDom.v, RecCoind.v |
| (Prelim) Tuesday 19th of Apr @ 16:00 | Chapter 8: More dependent types | Niels van der Weide | HG02.028 |
Useful links
- CPDT official website, latest pdf version, exercises
- Coq reference manual
- Coq Survival Kit by David Pichardie and Sandrine Blazy
- Cheatsheet by Andrej Bauer
