| Hôtel d'Orsay |
| 2 r François Leroux 91400 ORSAY |
| 01 64 86 17 47 |
| Hotel du Mont Blanc |
| 28, rue de la Huchette 75005 Paris |
| 01 43 54 22 29 |
| Wednesday April 23th | ||
| 13:00 | Coffee | |
| 14:00 | Philippe Audebaud | A Coq interface using TeXmacs |
| 14:45 | Claudio Sacerdoti | Metadata in Action: How to Query the Contribs of Coq |
| 15:30 | Break | |
| 16:00 | Benjamin Monate | Coqide : a new integrated Coq interface |
| 17:00 | Discussion | |
| Thursday April 24th | ||
| 9:00 | Coffee | |
| 9:30 | David Delahaye | Languages to Describe Proofs and Automations |
| 10:15 | Freek Wiedijk | Do we want a Mizar-mode for Coq? |
| 11:15 | Henk Barendregt | Aspects of mathematician-friendlyness |
| 12:00 | Lunch | |
| 13:00 | Coffee | |
| 13:30 | Yann Coscoy | Introducing natural language in proof development |
| 14:15 | Luiz Cruz-Filipe | What do we want from a documentation tool? |
| 15:00 | Claudio Sacerdoti | The MoWGLI Architecture and Tools for the Rendering of Coq Theorems |
| 16:00 | Discussion | |
We make a comparison between three proof styles: the procedural, the declarative and the term style (based on Curry-Howard's isomorphism). From this comparison, we show that these three styles are really appropriate for specific domains and we propose a new proof language, called Lpdt, which combines these three styles. This language has been implemented, as a prototype, in the Coq proof system and can already run some relevant examples. We present also the language Ltac which is already part of Coq and which allows us to extend quite easily the automation of the system. Currently, this language is based on a functional core with recursors and elaborated pattern-matching operators (for terms but also for proof contexts). With this proof dedicated meta-language, the user has a better control of the notion of triviality because he can provide, in a high-level way and more directly, tactics solving automatically some parts of proofs which are supposed to be trivial.
First I'll explain what a "Mizar mode" is. Then I'll show my Mizar mode for the HOL Light system. Finally I'll tell what is the main unsolved problem (according to my experience with my HOL Light Mizar mode) that is in the way of having a Mizar mode for Coq.
When building large libraries of formalized mathematics, it is very important to provide adequate documentation for these to help with their maintenance and future development. The experience with the C-CoRN library at the University of Nijmegen has shown that, unfortunately, existing tools are insufficient or not flexible enough for our needs. In this talk I will discuss some of the tools available for Coq and how they could and should be improved.
We briefly present the work done in the MoWGLI (Math on the Web: Get It by Logics and Interfaces) project to render Coq proof objects in HTML and MathML Presentation. The Coq proofs are first exported to XML using the Coq XML exportation module and then they are transformed into the OMDoc format by means of XSLT stylesheets; the OMDoc format can later on be rendered to HTML or MathML Presentation. The approach follows the one of Coscoy, but it has been extended to recognize other proof habits (e.g. forward vs backward reasoning steps, chains of reasoning, etc.) and to support the usual mathematical notation. Several problems are still open. In particular the rendering of the CCoRN (Coq Constructive Repository of Njimegen) is still highly unsatisfactory. These problems will be briefly summarized.
GNU is a free scientific text editor. It allows you to write structured documents via a wysiwyg and user friendly interface. New styles may be created by the user. The program implements high-quality typesetting algorithms and TeX fonts, which help you to produce professionally looking documents. It can be esaily extended by writing new styles or Scheme scripts. Thus, by many of its features, is suitable as an interactive development environment for the proof assitant Coq. We investigate this connection following three topics:
* Documentation: the goal is the importation of a Coq script into the native format, allowing thus the documentation of this proof script and the edition of a article from the raw data contained in the script.
* Working Session for Coq: we propose the use of the existing session mode to communicate with the proof assistant for the interactive development of proofs. In this mode, the interface benefits from all the editing facilities and high display quality of .
* Full Integration of Coq: in this environment, the goal is to hide as far as possible the Coq process; thus the user view gets closer to a paper sheet development.
The presentation will mainly focus on the first point. We point out the problems due to the conversion from the script into and our choices: importation format in , contents vs presentation, tasks schedule. The various aspects will be illustrated by examples. The results will be shown on the Coq Standard library and the Nijmegen FTA development.
The Coq system provides only limited searching functionalities (basically Search and SearchPattern). Moreover they can be used only on the modules that have been Required. In this talk we show a tool to effectively search at once all the contribs of Coq. The approach followed is the following: 1) the library is indexed by automatically extracting metadata that capture invariants of the matching procedure 2) when a query is issued giving a pattern, we compute a new approximate query over the computed metadata. The result of the query over the metadata is a set of matching candidates that is only a small subset of the whole library. Unification can later on be performed to extract the results from the set of candidates. The queries we support are a strict superset of the Coq ones.
This document was translated from LATEX by HEVEA.