osa1 - coq

osa1

Two challenges for dependently typed languages - September 23, 2014
Problems with tactic generated programs - September 13, 2014
Proving sorting algorithms correct - September 8, 2014
Coq exercises for beginners - July 12, 2014
A complicated proof of a simple theorem - July 10, 2014
Proving soundness of simply typed multi-staged lambda-calculus - March 6, 2014
On proof automations -- part 3 - September 23, 2013
On proof automations -- part 2 - September 17, 2013
On proof automations - September 11, 2013