Return to Article Details An Introduction to Programming and Proving with Dependent Types in Coq Download Download PDF