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