Tic tac types: a gentle introduction to dependently typed programming (functional pearl).

Sean Innes, Nicolas Wu

Browse the full ICFP paper archive.