Talk "The art of lying, with the proof assistant Coq"

by Dominique Duval

Wed, 03 September 2014 at 11:30 am in Sinaia, Romania

Joint work with: Jean-Guillaume Dumas, Burak Ekici, Jean-Claude Reynaud and Damien Pous

Abstract: A "lie-to-children" is a simplified explanation of technical or complex subjects as a teaching method for children. This method can also be used for adults, as well as for programs. In this talk it is used in different ways (dynamic evaluation, computational effects) for computing the rank of a matrix. The Coq implementation of the corresponding proofs is briefly presented.