COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Scaffolds and frames: the MathComp algebra formal library

## Scaffolds and frames: the MathComp algebra formal libraryAdd to your list(s) Download to your calendar using vCal - Georges Gonthier (INRIA Saclay - Île-de-France)
- Thursday 13 July 2017, 09:00-10:00
- Seminar Room 1, Newton Institute.
If you have a question about this talk, please contact INI IT. BPRW01 - Computer-aided mathematical proof It is commonplace to assert that a formalization library provides aframework for formal proof development – the resusable pieces offormalized mathematics that can be reassembled to build largertheories. This role is sometimes over emphasized by the “prooflibrary” moniker, implying that the main use of the library is toavoid duplicating proof work. However, our own experience with the MathComp library refutes thislimited view. First, most proofs in the more useful theories are veryshort, which shows that the structural elements afforded by a theory,such as concepts, combinators, or notation, can be more important thanthe “proof savings”. Second, some of the more useful things providedby our library don't even qualify as mathematical theories. They arebits of scaffolding, ranging from naming conventions and scriptingidioms to syntax metatheories, that help build new theories withoutproviding any identifuable parts thereof. This talk is part of the Isaac Newton Institute Seminar Series series. ## This talk is included in these lists:- All CMS events
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
- bld31
Note that ex-directory lists are not shown. |
## Other lists"Investigating Interactions" Symposium Faculty of Divinity Monday Mechanics Seminars (DAMTP) CamCreative Enterprise Tuesday 2016-2017 Spanish Researchers in UK (SRUK)-Cambridge## Other talksA cabinet of natural history: the long-lost Paston collection Source-and-Sink Models for Molecular Conduction Physico-chemical biology in practice, 1920s–1930s Investigation into appropriate statistical models for the analysis and visualisation of data captured in clinical trials using wearable sensors Nonstationary Gaussian process emulators with covariance mixtures Production Processes Group Seminar - "Evanescent Field Optical Tweezing for Synchrotron X-Ray Crystallography" |