osa1
github
gitlab
twitter
cv
rss
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 multistaged lambdacalculus

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