University of Cambridge > > Isaac Newton Institute Seminar Series > Concise - a synthesis of types, grammars, semantics

Concise - a synthesis of types, grammars, semantics

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact

BPR - Big proof

(joint work with Peter Schodl, Ferenc Domes, Kevin Kofler, Andreas Pichler, and David Langer, Vienna)

This talk features the design and implementation of tools that my research group in Vienna has created to pave the way towards automatically or interactively extracting from standard mathematical literature (such as the latex source of mathematics textbooks) a formal version of all  (correct and incorrect) mathematical claims contained in it, including all claims in the proofs and all implicit information needed for their understanding. We have very encouraging performance results for certain low level partial goals in this direction.

Completing this program (which I believe to be feasible with <50 man years of work) would produce a huge repository of formal statements and proof sketches ready for being formally proofchecked (possibly after completion or correction) by the formal theorem proving community.
Thus it would bridge the mathematicians' side of the current gap between mathematics and formal theorem proving.

Central to everything are the working implementation of

  • (i) a very flexible type system that merges types, grammars, and semantics into an organic unity, and
  • (ii) a dynamic parser for languages that change while reading a document – one of the key features present in mathematical documents.
Background (and, in the near future, more results) can be found on the project web page: neum/FMathL.html">

This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2017, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity