An Introduction to Programming and Proving with Dependent Types in Coq

Adam J. Chlipala. An Introduction to Programming and Proving with Dependent Types in Coq. J. Formalized Reasoning, 3(2):1-93, 2010. [doi]

Abstract

Abstract is missing.