Software foundations Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătǎlin Hriţcu, Vilhelm Sjöberg, Brent Yorgey [Google Scholar] [DBLP] [Citeseer] [url] Version 4.0. Electronic textbook 2016 Note(s): Coq theorem prover