|
|
4. Schedule Of The Congress
There is a long version of this schedule, including abstracts .
Wednesday, April, 30 9: Opening of the congress Programming Language design. 9.30-10. Containers and their derivatives. Thorsten Altenkirch . 10-10.30. Inductive familes need not store their indices. Edwin Brady .
10-10.30. Coffee break.
11-11.30. Epigram: an overview. Conor McBride . Co-author: James McKinna. 11.30-12. Type Inference for Nested Self Types. Viviana Bono . Co-authors: Jerzy Tiuryn, Pawel Urzyczyn. 12-12.30. Specification and Verification of Programs With Nested Datatypes:Illuminating Examples. Ralph Matthes , University of Munich.
12.30-14 Lunch
Formalizing Theories. 14-14.30. Formalization of Imperative Object-Calculi in (Co)Inductive Type Theories. Alberto Ciaffaglione . co-authors: Luigi Liquori, Marino Miculan. 14.30-15: C-CoRN, the Constructive Coq Repository of Nijmegen. Luís Cruz-Filipe . Co-author: Herman Geuvers. 15-15.30. Typed Ambients in Coq. Ivan Scagnetto . Co-author: Marino Miculan
15-15.30. Coffee break.
16-16.30. An operational formalization of square matrices in Coq. Nicolas Magaud (INRIA Sophia). 16.30-17. Nested Data Types in Constructive Type Theory. Peter Aczel .
Thursday, May, 1. Logical Frameworks. 9-10. Invited talk: A Concurrent Logical Framework. Pfenning Frank . 10-10.30. A Logical Framework with Dependently Typed Records. Authors: Coquand, Pollack, Takeyama .
10.30-11. Coffee break.
11-11.30. PAL+, a lambda-free logical framework, and its implementation. P.C. Callaghan, Yong Luo, and Z. Luo . 11.30-12. A Modular Approach to Logical Frameworks. Robin Adams . 12-12.30. A Framework for Typed HOAS and Semantics. Marino Miculan and Ivan Scagnetto .
12.30-14 Lunch
Type System Design . 14-14.30. Modules in Coq with rewriting. Jacek Chrzaszcz . 14.30-15. Combining Testing and Proving in Dependent Type Theory. Qiao Haiyan . Co-authors: Peter Dybjer, Makoto Takeyama 15-15.30. Induction and Co-induction in Sequent Calculus. Alberto Momigliano . Co-authors: Dale Miller, Alwen Tiu
15.30-16: Coffee break.
16-16.30. Why: a multi-language multi-prover verification tool. Jean-Christophe Filliatre (LRI, Université Paris Sud) 16.30-17. Rank 2 itersection types for modules. Damiani Ferruccio .
17.30-19.30 BUSINNES MEETING
Friday, May 2 Constructivism. 9-10. Invited Talk. Are the objects of propositional attitudes propositions in the sense of propositional and predicate logic? P. Martin Lof . 10-10.30. TBA. Giovanni Sambin .
10.30-11. Coffee break.
11-11.30. TBA. Berardi Stefano . 11.30-12. Witnesses in Constructive Analysis. Helmut Schwichtenberg . 12-12.30. Induction and co-induction at work in formal topology. S. Valentini . Co-author: M.E.Maietti.
Category Theory. 12.30-13. Abstract Stone Duality. Paul Taylor .
12.30-14 Lunch
Type Theory and Semantic . 14-14.30. Reduction Systems and Isomorphisms of Types. Sergei Soloviev . Co-author: David Chemouil 14.30-15. Set-theoretic Functors. Furio Honsell . Co-author: Daniela Cancila, Marina Lenisa. 15-15.30. Incomplete Proofs and Terms. G. Jojgov .
16-16.30. Coffee break.
16-16.30. Classical proofs and typed processes. Silvia Ghilezan (University of Novi Sad, Serbia). Co-author: Pierre Lescanne (Ecole Normale Superieure de Lyon, France). 16.30-17. Termination of rewriting in the Calculus of Constructions. Daria Walukiewicz-Chrzaszcz .
19.30: SOCIAL DINNER.
Saturday, May, 3 Linguistic. 9-9.30. Type Theory on a PDA: From Grammars to Gramlets. Kristofer Johannisson . Co-authors: Markus Forsberg, Janna Khegai, Aarne Ranta. Formalizing Proofs . 9.30-10. Extracting Test Cases from Correctness Proofs. Savi Maharaj . Co-author: Jeremy Bryans 10-10.30. Examples of applications of a proof assistant: From free modules on principal rings to a boiler. Frédéric Ruyer , université de Chambéry.
10.30-11. Coffee break.
11-11.30.Formal proof sketches versus Lamport-style proof. Freek Wiedijk . 11.30-12. Formalizing Higman's lemma in Isabelle. Stefan Berghofer (Muenchen) . Co-author: Monika Seisenberger (Swansea). 12-12.30. Program extraction from large proof developments. Bas Spitters . Co-authors: Luis Cruz-Filipe.
12.30-14: lunch.
Demo Session : 14-15.30. Demos runs in parallel. PAF!, a proof assistant for ML programs verification. Sylvain Baro, Yves Legrangérard , PPS, Université Paris 7. A prototype of PAL+, a lambda-free logical framework. P.C. Callaghan, Y. Luo, and Z. Luo. Epigram: the story so far. Conor McBride. Co-author: James McKinna. Tmcoq: Coq Integration within TeXmacs. Philippe Audebaud . Modules in Coq 7.4. Jacek Chrzaszcz . Co-author: Pierre Letouzey.
15.30-16: coffee break.
Optional Session (extra room for demos and talks) : 16-17.
Conferences and some demos will take place in Room A, using a projector. In Room B there are 10 cables with IP number: you may use them for demo and mail, but you need your own laptop. In Room C there are 20 computers ranged in a classroom, for mail and experimenting with proof assistants. A projector is available for demos. |
|
