Media type: E-Article Title: Interactive Theorem Proving: Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq Contributor: Forster, Yannick; Smolka, Gert Published: Springer International Publishing, 2017 Published in: Interactive Theorem Proving (2017), Seite 189-206 Language: Not determined DOI: 10.1007/978-3-319-66107-0_13 ISSN: 0302-9743; 1611-3349 Origination: Footnote: