Français
Proof and computation in Coq
Multi angle
Authors : Théry, Laurent (Author of the conference)
CIRM (Publisher )
68Q60 - Specification and verification (program logics, model checking, etc.)
68T15 - Theorem proving (deduction, resolution, etc.)
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
CIRM (Publisher )
Loading the player...
|
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.
MSC Codes : 68Q60 - Specification and verification (program logics, model checking, etc.)
68T15 - Theorem proving (deduction, resolution, etc.)
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
|
Information on the Video
Film maker : Hennenfent, GuillaumeLanguage : English Available date : 03/02/16 Conference Date : 14/01/16 Subseries : Research talks arXiv category : Computer Science ; Logic in Computer Science Mathematical Area(s) : Computer Science Format : MP4 (.mp4) - HD Video Time : 00:56:59 Targeted Audience : Researchers Download : https://videos.cirm-math.fr/2016-01-14_Thery.mp4 
|
Information on the Event
Event Title : Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certificationEvent Organizers : Mahboubi, Assia ; Schuster, Peter ; Spitters, Bas Dates : 11/01/16 - 15/01/16 Event Year : 2016 Event URL : http://conferences.cirm-math.fr/1508.html
Citation Data
DOI : 10.24350/CIRM.V.18915003Cite this video as: Théry, Laurent (2016). Proof and computation in Coq. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.18915003 URI : http://dx.doi.org/10.24350/CIRM.V.18915003 |
See Also
- [Multi angle] Verified numerics for ODEs in Isabelle/HOL / Author of the conference Immler, Fabian.
- [Multi angle] Programming with numerical uncertainties / Author of the conference Darulova, Eva.
- [Multi angle] Formal verification of numerical analysis programs / Author of the conference Boldo, Sylvie.
- [Post-edited] Wrapping in exact real arithmetic / Author of the conference Müller, Norbert.
Bibliography
