TY - BOOK AU - Chlipala TI - Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant PB - IEEE UR - https://ieeexplore.ieee.org/servlet/opac?bknumber=6712486 ER -