Archives
- December 25, 2019 Quotients in Coq
- December 24, 2019 A verification challenge
- August 6, 2019 Contravariance and Recursion
- October 15, 2018 Checking for Constructors
- January 26, 2018 Equality in Coq
- March 14, 2016 POPL and CoqPL 2016
- April 13, 2015 Writing reflective tactics
- April 6, 2015 Two nice Coq-related blogs
- March 25, 2015 Analyzing sorting algorithms
- October 26, 2014 Coq as its own extensible parser
- July 15, 2014 Searching with eggs
- November 17, 2013 Automatic naming considered harmful
- October 27, 2013 Summing combinatorial games
- September 8, 2013 An introduction to combinatorial game theory
- June 27, 2013 Structuring proofs with bullets
- May 6, 2013 A smarter constructor tactic
- April 19, 2013 Type-safe printf in Coq
- April 18, 2013 New domain
- April 3, 2013 Parse errors as type errors
- March 31, 2013 Reading and writing numbers in Coq
- March 30, 2013 Welcome