DTP 2008

Dependently Typed Programming

NCSL, Jubilee Campus, University of Nottingham, UK, 18 - 20 February, 2008



Sunday 17th February

18.00Pub the Three Wheatsheves

Monday 18th February

09.00Registration and Welcome

09.30  Why dependent types matter
   Thorsten Altenkirch (University of Nottingham)
10.00  Dependently Typed DSLs for Resource Usage Verification
   Edwin Brady (University of St. Andrews)


11.00  Ecce isn't Epigram2
   Peter Morris (University of Nottingham)
11.30  Dependent Finger Trees
   Matthieu Sozeau (LRI)

12.00Lunch in the Restaurant

14.00  Derivation-Carrying Code using Dependent Types
   Shin-Cheng Mu (Academia Sinica, Taiwan)
14.30  Interactive Programs and Coalgebras
   Anton Setzer (Swansea University)

15.00Coffee and Discussion

16.00  Supporting the Development of Dependently Typed Functional Programs
   Sean Wilson (Edinburgh University)
16.15  Talk 'Bout Agda
   Ulf Norell (Chalmers University of Technology)
16.45  Structurally Recursive Descent Parsing
   Nils-Anders Danielsson (University of Nottingham)


Tuesday 19th February

09.00  Programming a compiler with a proof assistant: an experience report (invited talk)
   Xavier Leroy (INRIA, Paris-Rocquencourt)
10.00  Verifying a Semantic beta-eta-Conversion Test for Martin-Loef Type Theory
   Andreas Abel (University of Munich)


11.00  A core theory for Dependently Typed Programming
   Nicholas Oury (University of Nottingham)
11.30  Delphin: Practical programming with HOAS and Dependent Types
   Adam Poswolsky (Yale University)

12.00Lunch in the Restaurant

14.00  Programming with nested datatypes through dependent types
   Ralph Matthes (IRIT (CNRS and University of Toulouse III))
14.30  Machine-Independent Code Certification with the LF Type Theory
   Nicholas Magaud (University of Strasbourg)

15.00Coffee and Discussion

16.00  TBA
   Stephanie Weirich (CMU)
16.15  Can dependently typed programming succeed? (invited talk)
   Lennart Augustsson (Credit Suisse)


19.30Conference Dinner in the Restaurant

Wednesday 20th February

09.00  Polarity and duality in type theory
   Noam Zeilberger (CMU)
09.30  Power of Pi
   Wouter Swierstra (University of Nottingham)
10.00  The Implicit Calculus of Constructions (ICC*)
   Bruno Bernardo (Ecole polytechnique, INRIA Futurs)


11.00  Dependent Types for Modelling and Simulation: Challenges and Opportunities
   Henrik Nilsson (University of Nottingham)
11.30  Generalizing Dependent Inductive Datatypes to Specify the Static Semantics of Programming Languages
   Christian Stork (UCI)
12.00  Data, Deliberately
   Conor McBride (Alta Systems)