| 9:00-9:15 | Chair's welcome |
| SESSION I, 9:15-10:15 | |
|---|---|
| 9:15-10:15 | Invited talk by Michael Warren: Univalence and the formalization of mathematics in Coq. |
| BREAK, 10:15-10:45 | |
| SESSION II, 10:45-12:15 | |
| 10:45-11:15 | Benjamin Berman, New Coq User Interfaces: Survey and Ideas. (Co-authors: Aaron Stump and Juan Pablo Hourcade) |
| 11:15-11:45 | Enrico Tassi, Designing a state transaction machine for Coq. (Co-author: Bruno Barras) |
| 11:45-12:15 | Short presentations and discussion about university teaching using Coq. Speakers for 10-minute talks: Christopher Dutchyn, Adam Chlipala |
| LUNCH, 12:15-13:45 | |
| SESSION III, 13:45-15:15 | |
| 13:45-14:30 | Invited talk by Hugo Herbelin: Coq team report on the latest developments. |
| 14:30-14:50 | Cyril Cohen, Reasoning about big enough numbers in Coq. |
| 14:50-15:15 | Yves Bertot, Removing the axiom "sin(PI/2) = 1" from Coq's library of real numbers. |
| BREAK, 15:15-15:45 | |
| SESSION IV, 15:45-17:30 (approximately) | |
| 15:45-16:10 | Thomas Braibant, Formal verification of hardware synthesis. (Co-author: Adam Chlipala) |
| 16:10-16:35 | Gregory Malecha, Building Bedrock: Verifying a Program Verifier. (Co-authors: Adam Chlipala, Thomas Braibant, Patrick Hulin, and Edward Z. Yang) |
| 16:35-17:30 | Short presentations and discussion about computation inside Coq. Speakers for 10-minute talks: Maxime Dénès, Andrew Kennedy, Magnus Myreen |
| RECEPTION, 18:00-? | |
In this talk we will provide an exposition of recent research relating relating homotopy theory and type theory, with the main focus on Voevodsky's Univalent Foundations. The talk will be divided roughly into two parts. In the first part we will give a somewhat gentle introduction to Univalent Foundations aimed at Coq users. In the second part we will offer some observations based on our experiences over the past year developing Coq libraries in the setting of Univalent Foundations and teaching Coq to mathematicians coming to Coq from outside of logic and theoretical computer science.
In December 2011 we invited Coq-Club mailing list subscribers to fill out an online survey, asking for their opinions about and experiences with existing Coq user interfaces and for their ideas regarding new interfaces. Our motivation was to validate our ideas about new Coq user interfaces, and to generate new ones. We received 48 responses, including many detailed responses to the essay questions in the survey. Here we present a summary of these responses, along with some of the ideas that motivated them originally.
The Paral-ITP project aims at bringing to ITPs users the benefits of a modern user interface. Its main characteristic will be to drop the locked-region paradigm of Proof General, as well as the read/eval/print loop on which it is based. The main benefit is that the system will let the user edit his document at any place and will still be able to give interactive feedback on any other portion of the document. To do so we need to rethink the way an ITP processes the document the user is editing to obtain an asynchronous and more reactive system. This will also pave the way to a systematic use of modern, parallel, hardware to achieve better performances. In this talk we will discuss the main ingredients of the recipe, we will report on the ongoing implementation and we will wet the audience appetite with a demo.
High-level languages provide abstractions that assist programmers; however, these abstractions are not always sufficient and, in some cases, they get in the way of writing efficient or correct code. In this talk we discuss the development of Bedrock, a Coq framework for foundational verification of low-level programs. Bedrock combines reflective algorithms for symbolic execution, a separation logic prover, and a collection of base theory provers for reasoning about, for example, lists and machine words. These algorithms must reason about quantifiers and meta-variables and their interaction with separation logic and our language semantics.
We focus on the most interesting bits of our use of computational reflection. In particular, we discuss a style of phrasing correctness statements that enables composing multiple verification algorithms about different theories in a reasonable way. In addition, we consider the performance implications of some high-level design choices and lower-level implementation details including: the representation of reified terms and the reification process, the use of dependent functions, the ability to control reduction, and the phrasing of lemmas to simplify proof checking.