Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certification

Collection Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certification

Organizer(s) Mahboubi, Assia ; Schuster, Peter ; Spitters, Bas

Date(s) 11/01/2016 - 15/01/2016

linked URL http://conferences.cirm-math.fr/1508.html

00:00:00 / 00:00:00

5 5

Proof and computation in Coq

By Laurent Théry

Also appears in collection : Exposés de recherche

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.

Information about the video

Date of recording 14/01/2016
Date of publication 03/02/2016
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers
Director(s) Guillaume Hennenfent
Format MP4

Citation data

DOI 10.24350/CIRM.V.18915003
Cite this video Théry, Laurent (14/01/2016). Proof and computation in Coq. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.18915003
URL https://dx.doi.org/10.24350/CIRM.V.18915003

Domain(s)

MSC codes

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

All the collection videos

57:56

published on February 4, 2016

Formal verification of numerical analysis programs

By Sylvie Boldo

59:51

published on February 3, 2016

Wrapping in exact real arithmetic

By Norbert Müller

46:54

published on February 3, 2016

Programming with numerical uncertainties

By Eva Darulova

01:01:17

published on February 3, 2016

Verified numerics for ODEs in Isabelle/HOL

By Fabian Immler

56:59

published on February 3, 2016

Proof and computation in Coq

By Laurent Théry

Copyright Carmin.tv 2024

Give feedback