| 09:00-09:30 | Judicaël Courant, Explicit Universes for the Calculus of Constructions
|
| 09:30-10:00 | Ana Bove, General Recursion in Type Theory
|
| 10:00-10:30 | Yves Bertot, A practical approach to general recursion in the Calculus of Inductive Constructions
|
| Coffee
|
| 11:00-11:30 | Yong Luo, Coherence and Transitivity in Coercive Subtyping
|
| 11:30-12:00 | Robert Kiessling, Coercive Subtyping for Hindley-Milner Type Systems
|
| 12:00-12:30 | Maria Joao Frade, Type inference with constructor subtyping
|
| Lunch
|
| 14:00-14:30 | Xingyuan Zhang, Focus Constructively -- A Lightweight Approach for Concurrency in Type Theory
|
| 14:30-15:00 | Jianmin Pang, Paul Callaghan and Zhaohui Luo, An approach to verification of domain properties based on LF
|
| 15:00-15:30 | Michal Konecny, Refining of Linear Types for In-Place Update
|
| Tea
|
| 16:00-16:30 | Benjamin Gregoire, Compiling Proofs
|
| 16:30-17:00 | Pierre Letouzey, A new extraction for Coq
|
| 17:00-17:30 | Stefan Berghofer, Program extraction in Isabelle
|
| 17:30-18:30 | DEMOS:
|
| Demo Pierre Letouzey, Examples of extraction in Coq
|
| Demo Stefan Berghofer, An implementation of program extraction in Isabelle
|
| Demo Paul Callaghan, Implementation of coercion rules
|
| Demo Markus Wenzel, Notable concepts in contemporary Isabelle
|
| Demo Yves Bertot, PCoq
|
| Demo Adam Grabowski and Adam Naumowicz, How to use types in Mizar
|
|
|
| 20:30-21:30 | Business Meeting
|