Page under development
Back to MathWiki main page

Talks offered so far (in no particular order)

  • Klaus Grue (invited talk) (slides)
    One would have expected that all of mathematics would have been machine 
    formalized some decades after the invention of the digital computer. But 
    it seems that something has been missing for that to happen.
    Logiweb ( was conceived in an attempt to analyse what 
    was missing. And it was designed and implemented 1996-2006 to meet the 
    following objectives:
    Accumulation of knowledge: Once a machine formalized development was 
    published on Logiweb, the publication should remain accessible in 
    unchanged form forever. This simply mimics what publishing houses and 
    libraries provide for ordinary mathematics.
    Standing on the shoulders of predecessors: When proving a theorem, users 
    should be able to draw upon theorems proved by others. This simply mimics 
    the way any mathematician works.
    Notational freedom: Each user should be free to use any notation. That 
    freedom should come without restricting the notational freedom of others. 
    And differences in notation should be no obstacle when using the results 
    of others.
    Foundational freedom: Each user should be free to choose what mathematical 
    foundation to work upon. Import of results from one foundation to another 
    should be possible (but not neccessarily trivial).
    Distribution: Access to the work of others should happen transparently via 
    the Internet.
    Readibility: Users should be able to publish articles on Logiweb which are 
    as readable as any mathematics book one can pick from any library.
    Accommodation: Users should be able to publish anything from short notes 
    to multi-volume works that span thousands of pages.
    Scalability: The system should allow an arbitrary number of submissions 
    and should run smoothly up to 10^18 papers.
    Simplicity: The system should be so simple that its core could be 
    implemented by a single person. And so simple that once it was 
    implemented, a graduate computer science student could re-implement it in 
    one year.
    Extensibility: Once the core was implemented, users should be able to 
    adapt the system without changing the core and should be able to publish 
    adaptations on Logiweb itself to make the adaptations available to other 
    Verification: Logiweb should be able to tell whether or not a publication 
    is correct. In the spirit of accumulation, correctness should be time 
    independent such that a publication which is deemed correct at one time 
    should remain correct forever.
    Logiweb is a rather simple system which fulfills the objectives above. The 
    talk gives a walk-through of the system. Furthermore, the talk describes 
    how Logiweb can interface to other systems like wiki systems and other 
    proof systems.
  • Loïc Pottier
    talk/demo on Wikicoqweb: Proofs for freshmen with Coqweb
    Coqweb is a web interface for Coq, primarily designed for teaching. It
    allows teachers to propose statements in sufficiently familiar
    form. Students are invited to prove these statements essentially by
    clicking. Hints can be given in natural language, in which case the
    interface checks that the student somehow understands the hints. We
    present here the main features of Coqweb, and show through examples
    how it has been used since 2004.
  • Zhaohui Luo (slides)
    Formal Reasoning with Different Logical Foundations
  • Adam Naumowicz (slides)
    We will present the key aspects of the Mizar technology for formalizing
    mathematics as well as building and maintaining a database of formalized
    and semantically linked knowledge - Mizar Mathematical Library. We will
    focus on the issues relevant to the WWW environment: XML-based
    presentation, querying with MMLQuery and on-line processing of Mizar
  • Carsten Schürmann (slides)
  • Makarius Wenzel (slides)
    Asynchronous processing of proof documents -- rethinking interactive theorem proving
    The classical model of interactive proof-checking is best illustrated by 
    the de-facto standard user-interface, namely Proof General. Here the user 
    operates on a collection of theory files, while editing the body of a 
    single theory works by stepping back and forth in a strictly sequential 
    (synchronous) fashion.
    I would like to take a fresh look at how proof documents are processed. 
    Both the increased demands of large formalizations should be addressed, as 
    well as multi-processing that has become readily available now. 
    Ultimately, user-interfaces and related prover protocols with the 
    following characteristics should emerge:
      - Less requirements on the "editor" component, i.e. make it work with 
        simple web interfaces, rather than demanding a "rich client" 
      - The prover should be able to re-order and re-schedule individual 
        theory and proof transactions according to their inherent 
      - The user should be able to edit theory sources very freely, with the 
        system maintaining consistency as expected. Here the inherent 
        structure of a proof language like Isar admits the outline to be 
        checked quickly, while the sub-proofs may be refined later by 
        iterative deepening.
      - Editing of unfinished, partially broken theories and proofs should be 
        easy (in fact the norm rather than the exception).
    Thus we hope to increase effectiveness of interactive theorem proving 
    significantly, enabling users to work on much larger formalizations.
  • Christoph Lüth (slides)
    Collaborative Editing with PGIP
    We will give a fresh view on the display side of the PGIP protocol,
    which connects interface front-ends (called displays) with the central
    PGIP middleware (and hence the provers). This stateless display protocol
    can be conveniently modelled as a REST-style interface with XUpdate
    messages signalling changes. From there, we discuss possibilities for
    collaborative editing in this context-- it turns out that collaborative
    editing is more or less built in, but needs to be restricted to make it
  • Herman Geuvers (slides)
    Challenges to a global web-based library of formal mathematics
    (Based on discussions with Cezary Kaliszyk and Pierre Corbineau)
    I will discuss what I perceive to be the possibilities for developing a 
    "Wiki for Formalized Mathematics" within a joint European ICT project.
    I see two main motivations for such a system:
    - Cooperative work on a large repository of formalized mathematics. This 
    is also to solve the problem that "there is not enough mathematics 
    - Providing high level access to a repository of formal maths. When 
    searching for a mathematical notion, one should also get a 
    comprehensible link to the formalization. This should also help solve 
    the "access problem": what is in the repository?
    In the talk I will discuss what could be done and what I think should be 
    done. Audience participation during the talk is very much appreciated.
  • Aarne Ranta (slides)
    Documenting and Editing Formal Mathematics in Natural Language
    - GF: translations between languages (both formal and natural)
    - GF Resource Grammar Library: high-level programming of  
    grammatically correct translation rules
    - embedded grammars in JavaScript: automatic generation of  
    multilingual syntax editors from GF grammars
    - using embedded JavaScript grammars in Wiki pages
  • Cezary Kaliszyk (slides)
    Teaching logic using a web interface for Coq
    We will present the system ProofWeb, that allows teaching students
    logic using an interactive web interface to the proof assistant Coq.
    First we will present a general framework for creating responsive web
    interfaces to proof assistants, which allows the students to use the
    system without the need to install anything (not even a browser
    plug-in). On top of that we will present an extension for teaching,
    that makes the full power of Coq available to the students, but
    simultaneously presents the logic problems in a way that is customary
    in undergraduate logic courses. Both styles of presenting natural
    deduction proofs (Gentzen-style `tree view' and Fitch-style `box
    view') are supported. The system allows the teachers to centrally
    track progress of the students. We will present a database of logic
    problems, that also holds the students solutions and a parser that
    indicates whether the students used only the allowed inference rules
    of the logic.
  • Pierre Corbineau (slides)
    A prototype system for collaborative proving
    We present a framework for the online development of formalized
    mathematics. This framework allows wiki-style collaboration while
    providing users with a rendered and browsable version of their work.
    We describe a prototype for Coq, based on the web interface
    implemented by Cezary Kaliszyk (which he will present in his talk),
    and a modified version of the MediaWiki code-base.
    Then, we will focus on cross-file consistency and dependency issues
    with concurrent access and write, and finally on requirements for
    supporting existing proof assistants.
  • Lucas Dixon (slides)
    An Implicational Logic for Conjecturing and Distributed Proof Attempts
    I will introduce a logic of implication which supports making
    conjectures as a basic operation. This allows them to be used before
    they are proved as well as reused in different branches of a proof and
    in different parts of a theory. This forms a meta-theory for theories
    which allows distributed proof attempts while maintaining the
    interdependencies between lemmas. I hope to develop this into a full
    type theory which gives keeps support for distributed development.
  • Hugo Herbelin (slides)
    A glimpse of Evgeny Makarov's abstract and modular formalisation of arithmetic in Coq
    Evgeny Makarov formalised basic axiomatic arithmetic in Coq.  He came
    up with two sets of Peano-style axioms that characterise respectively
    natural numbers and integers and differ only in saying whether every
    number has a predecessor. Then he derived generic lemmas about "plus",
    "times", "less than" and a setoid equality. New functions can be
    defined generically using Peano's recursion or by axiomatising their
    defining properties and providing implementations of these properties
    for various datatypes (zero-and-successor numbers, binary numbers,
    etc.). Theorems proved from defining properties hold for every
    implementation. Automation such as polynomial simplification (the ring
    tactic) directly hold from the genericity of Barras-Gregoire-Mahboubi
    implementation. Generic decision of linear arithmetic (and beyond), is
    work in progress.
    From the "math wiki" perspective, we wonder whether focusing on a
    well-delimited mathematical theory such as the one used to formalise
    arithmetic, or more generally number theory, could provide an
    interesting first step to make both human beings and the different
    proof assistants agree on a common high-level domain-specific
    mathematical vernacular.
  • Freek Wiedijk (slides)
    Obstacles to a global library of formal mathematics
    I will discuss what I perceive to be the main reasons that there is
    not yet a large scale effort to create a good and comprehensive
    library of formal mathematics.
  • Alexander Konovalov (slides)
    Providing mathematical Web services with Symbolic Computation Software Composability Protocol
    Modern symbolic computations require infrastructure for parallel
    algorithms and combining capabilities available in several different
    systems.  Moreover, there are growing numbers of symbolic computation
    resources, such as databases or specialised software which could be
    made available as Web services or Grid services accessible over the
    Internet.  The EU Framework VI project "SCIEnce --- Symbolic
    Computation Infrastructure in Europe"
    ( addresses these needs of the
    symbolic computation user community.
    First we designed the Symbolic Computation Software Composibility
    Protocol (SCSCP) by which a computer algebra system (CAS) may offer
    services and a client may employ them. We envisage clients for this
    protocol including:
    - A Web server which passes on the same services as Web services
    using SOAP/HTTP protocols to a variety of possible clients;
    - Grid middleware;
    - Another instance of the same CAS (in a parallel computing context);
    - Another CAS running on the same computer system or remotely.
    All messages in the protocol are represented as OpenMath objects
    In my talk I will give more details about OpenMath and SCSCP, and will
    demonstrate some examples using SCSCP implementation for the
    computational algebra system GAP (

    Other people who will attend

  • Randy Pollack
  • Conor McBride
  • Stephane Lengrand
  • Bengt Nordstrom
  • Roy Dyckhoff
  • Peter Hancock
  • David Aspinall
  • James McKinna
  • Peter Chapman
  • Nik Sultana
  • Marcin Benke
  • Robert Rothenberg
  • Artur Kornilowicz
  • Clemens Ballarin
  • Paul Jackson
    Back to MathWiki main page
    Randy Pollack
    Last modified: Mon Nov 19 13:49:21 GMT 2007