Tree @master (Download .tar.gz)
Papers.md @master — view markup · raw · history · blame
Coq Papers
Recursive Datatypes and Inductive Proofs
- authors: unknown
- date: 2008
- format: lecture-notes
- online @ www.inf.ed.ac.uk
.
Interactive Theorem Proving with Coq
- authors: Adam Chlipala
- date: 2004
- format: talk-slides
- online @ people.eecs.berkeley.edu
.
Pragmatic Quotient Types in Coq
- authors: Cyril Cohen
- date: 2013
- online @ perso.crans.org
.
Interaction Trees
- subtitle: Representing Recursive and Impure Programs in Coq
- authors: Li-Yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
- date: 2020
- online @ archive.org
- future-topics: Formal Verification, Monads, Bisimulation
.