Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant - Chlipala, Adams, 1981- (MIT, 2013)