APA Style

CLIPALA, A. (2013). Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant . Cambridge: The MIT Press.

MLA Style

CLIPALA, Adam. "Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant". Cambridge: The MIT Press, 2013. Text.