BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Scaffolds and frames: the MathComp algebra formal library - George
 s Gonthier (INRIA Saclay - Île-de-France)
DTSTART:20170713T080000Z
DTEND:20170713T090000Z
UID:TALK73270@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:&nbsp\; It is commonplace to assert that a formalization libra
 ry provides aframework for formal proof development - the resusable pieces
  offormalized mathematics that can be reassembled to build largertheories.
  &nbsp\;This role is sometimes over emphasized by the "prooflibrary" monik
 er\, implying that the main use of the library is toavoid duplicating proo
 f work.&nbsp\; However\, our own experience with the MathComp library refu
 tes 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 than
 the "proof savings". Second\, some of the more useful things providedby ou
 r library don&#39\;t even qualify as mathematical theories. They arebits o
 f scaffolding\, ranging from naming conventions and scriptingidioms to syn
 tax metatheories\, that help build new theories withoutproviding any ident
 ifuable parts thereof.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR