CHIT/CHAT Workshop Program

CHIT Session 1 (Room GN3, Gymnasium Building)

• 9h00 - 9h30 Registration, Coffee

• 9h30 - 10h30 Carsten Schürmann (invited speaker) :
  Proof Directed Programming: Twelf --- A Case Study

• 10h30 - 10h45 Break

• 10h45 - 11h35 Randy Pollack
  An Introduction to the Constructive Engine
• 11h35 - 12h25 Conor Mc Bride
  An Overview (and an Underview) of Epigram 2

Lunch break (Cantine, Huygens Building)

CHIT Session 2 (Room HG00.075, Huygens Building)

• 14H00 - 15h30 Demo Session

• 15h30 - 15h45 Break

• 15h45 - 17h00 Hacking Session

17h00 Cocktail (2nd floor North Hallway, Huygens Building)

CHIT Session 3 (Room HG00.304, Huygens Building)

• 9h00 - 9h50 Wouter Swierstra
  Implementing Observational Equality in Epigram 2
• 9h50 - 10h40 Bruno Barras
  A syntactic criterion for checking termination of structural recursion in Coq

• 10h40 - 10h50 Break

• 10h50 - 11h40 Freek Wiedijk
  How to implement a type checker ?
• 11h40 - 12h30 Peter Morris
  A universe for data in Epigram 2

Lunch break (Cantine, Huygens Building)

CHIT Session 4 (Room HG00.303, Huygens Building)

• 13h50 - 14h40 Makarius Wenzel
  Generic contexts in Isabelle/Pure
• 14h40 - 15h30 Andreas Abel
  Abstract Values and NBE (normalization by evaluation) Techniques

• 15h30 - 15h45 Break

• 15h45 - 17h15 Discussion

19h30 Dinner (Café-restaurant Station Oost, Daalseweg 17)

CHIT Session 5 (Room HG00.303, Huygens Building)

• 8h50 - 9h40 Hugo Herbelin & Élie Soubiran
  A higher-order refinement-based module system
• 9h40 - 10h30 Ulf Norell
  A Module System for Agda

• 10h30 - 10h40 Break

• 10h40 - 12h30 Hacking session (Room 029)

Lunch break (Cantine, Huygens Building)

CHIT Session 6 (Room HG00.023, Huygens Building)

• 13h50 - 14h40 Claudio Sacerdoti Coen
  A presentation of Matita
• 14h40 - 15h30 Stefan Berghofer
  Proof terms in Isabelle

CHAT Session 1 (Rooms HG00.303 & HG00.023 , Huygens Building)

• 8h50 - 9h40 Serge Autexier
  PLATO: A Mediator between Text-Editors and Proof Assistance System
• 9h40 - 10h30 Claudio Sacerdoti Coen
  Automatic generation of procedural scripts.

• 10h30 - 10h45 Break (changing to room 023)

• 10h45 - 11h35 Bengt Nordstrom
  How to interact with a proof editor ?
• 11h35 - 12h25 Pierre Corbineau
  A Declarative Proof language for the Coq Proof Assistant

Lunch break (Cantine, Huygens Building)

CHAT Session 2 (Room HG00.303, Huygens Building)

• 13h50 - 14h40 Josef Urban
  Mizar and its User Interfaces
• 14h40 - 15h30 Lionel Mamane
  tmEgg: a document-oriented Coq-TeXmacs integration

• 15h30 - 15h40 Break

• 15h40 - 16h30 Cezary Kaliszyk
  A Web Interface for Proof Assistants and the Development of Formalized Mathematics Archives

CHAT Session 3 (Rooms HG00.075 & HG00.303, Huygens Building)

• 9h20 - 10h30 Demo Session

• 10h30 - 10h45 Break (changing to room 303)

• 10h45 - 11h35 Makarius Wenzel
  Isabelle/Isar: from Structured Proofs to Structured Specifications
• 11h35 - 12h25 Lucas Dixon
  Issues for Proof-Centric Proof Interfaces

Final lunch (Cantine, Huygens Building)