Laurent Théry : Proof and computation in Coq

Abstract : In this talk, we are going to show on some elementary examples how computation can easily be incorporated inside proof in a proof system like Coq.

Recording during the thematic meeting: "Effective analysis: foundations, implementations, certification" the January 14, 2016 at the Centre International de Rencontres Mathématiques (Marseille, France)

Filmmaker: Guillaume Hennenfent

Find this video and other talks given by worldwide mathematicians on CIRM's Audiovisual Mathematics Library: http://library.cirm-math.fr. And discover all its functionalities:
Chapter markers and keywords to watch the parts of your choice in the video
Videos enriched with abstracts, bibliographies, Mathematics Subject Classification
Multi-criteria search by author, title, tags, mathematical area