Scaffolds and frames: the MathComp algebra formal library

Speaker(s) Georges Gonthier INRIA Saclay - Île-de-France
Date 13 July 2017 – 09:00 to 10:00
Venue INI Seminar Room 1
Session Title Scaffolds and frames: the MathComp algebra formal library
Event [BPRW01] Computer-aided mathematical proof
Abstract   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.
Presentation Files 17967_0.pdf

Supported By