This repo contains the code, notes and other resources for a presentation that advertises the Coq programming language:
The slides:
- Are shared here: https://slides.com/awalterschulze/advertising-coq
- They contain all the speech as text
- They also contain links to the code that is shared here, which also contain the speech during the demo as comments
Creating these slides included watching a few videos and a brainstorming session, during which notes were taken, see Notes
The code:
- deMorgenBool.v
- Sum.v
- CurryHoward.v
- Book.v
- deMorgenProp.v (optional)
The code compiles with Coq version 8.12.0
This presentation was given at:
- Center for Experimental Mathematics, Stellenbosch University on 9 September 2020