The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


18.00  Buffet, Reception and Registration in the School of Computer Science 


21.00  Close 



07.30  Breakfast in the Catering Facility 


09.00  Structured Computations (invited talk) 

Bart Jacobs (Radboud Universiteit Nijmegen) 


10.00  Coffee and Registration 


10.30  Dataflow Analyses and Type Systems 

Tarmo Uustalu (Institute of Cybernetics, Tallinn) 
10.55  Type Theory in Sequent Calculus 

Stéphane Lengrand (University of St Andrews) 
11.20  Combined normal forms in sequent calculus 

Luís Pinto (Universidade do Minho) 
11.45  Embedding Pure Type Systems in the λΠcalculus 

Gilles Dowek (LIX  Ecole Polytechnique) 


12.10  Lunch in the Catering Facility 


14.00  The Nominal Datatype Package 

Christian Urban (LudwigMaximiliansUniversität, München) 
14.25  Types for Nominal Terms 

Maribel Fernandez (King's College London) 
14.50  Structured Induction Proofs in Isabelle/Isar 

Makarius Wenzel (Technische Universität München) 
15.15  Pattern Matching Coverage using Approximations 

Nicolas Oury (LRI Orsay) 


15.40  Coffee 


16.00  A Type Theory with Partially Defined Functions 

Yong Luo (University of Kent) 
16.10  Consistency and Completeness of Rewriting in the Calculus of Constructions 

Daria WalukiewiczChraszcz (Warsaw University) 
16.20  Dependent Type Theory with PatternMatching and SizeChange Termination 

David Wahlstedt (Chalmers University of Technology) 
16.30  A Practical Approach to Coinduction in Twelf 

Alberto Momigliano (LFCS, University of Edinburgh) 
16.40  Separability in Classical λCalculi 

Silvia Ghilezan (University of Novi Sad) 


16.50  Break 


17.00  Simple proofs of strong cutelimination 

José Espírito Santo (Universidade do Minho) 
17.10  Towards Automatization of Framed Bisimilarity in Coq 

Ivan Scagnetto (Università di Udine) 
17.20  Proof Methodologies for Behavioural Equivalence in Distributed πCalculus 

Alberto Ciffaglione (Università di Udine) 
17.30  Web Interface for Coq 

Cezary Kaliszyk (Radboud Universiteit Nijmegen) 
17.40  Demonat Project 

Patrick Thévenon (Université de Savoie) 
17.50  MultiLevel Lax Logic 

Mike Stannett (University of Sheffield) 


18.00  Close 


18.30  Dinner in the Catering Facility 



07.30  Breakfast in the Catering Facility 


09.00  To memory safety through proofs and beyond (invited talk) 

Hongwei Xi (Boston University) 


10.00  Coffee 


10.30  Dependently Typed Metaprogramming (TFP talk) 

Edwin Brady (University of St Andrews) 
10.55  An Implementation of a Compiler for a Dependently Typed Functional Programming Language 

Hiroyuki Ozaki (National Institute of Advanced Industrial Science and Technology) 
11.20  Proving Termination Using Dependent Types: the Case of XorTerms (TFP talk) 

JeanFrançois Monin and Judicaël Courant (VERIMAG) 
11.45  Few Digits: A Monadic Approach to Exact Real Arithmetic 

Russell O'Connor (Radboud Universiteit Nijmegen) 


12.10  Lunch in the Catering Facility 


14.00  The Poincaré Principle and ZFC Set Theory 

Freek Wiedijk (Radboud Universiteit Nijmegen) 
14.25  Type Theory as a Solution to the Proofs as Programs Problem 

Maria Emilia Maietti (Università di Padova) 
14.50  Weyl's Predicative Mathematics in Type Theory 

Zhaohui Luo (Royal Holloway, University of London) 
15.15  The Matita Proof Assistant 

ClaudioSacerdoti Coen + Enrico Tassi (Università di Bologna) 


15.40  Coffee 


16.00  Representation of partial recursive functions by inductiverecursive and by inductive definitions 

Anton Setzer (Prifysgol Cymru Abertawe) 
16.10  A BHK semantics that justifies classical logic 

Jens Brage (Stockholm University) 
16.20  Internalising Modified Realisability in Constructive Type Theory 

Erik Palmgren (Uppsala University) 
16.30  Isomorphisms and Coercive Subtyping in PAL+ 

Serguei Soloviev (IRIT, Toulouse) 
16.40  Isomorphisms for contextfree types 

Wouter Swierstra (University of Nottingham) 


16.50  Break 


17.00  The Equivalence of Convertibility and Judgemental Equality 

Robin Adams (Royal Holloway, University of London) 
17.10  An Interpreter for Intuitionistic Linear Logic Programs 

Alan Smaill (University of Edinburgh) 
17.20  A direct translation of the Simply Typed Lambda Calculus into C++templates 

Markus Michelbrink (Prifysgol Cymru Abertawe) 
17.30  A Games Semantics for Reductive Logic and ProofSearch 

Eike Ritter (Universiy of Birmingham) 
17.40  The Structure of Mizar Types 

Grzegorz Bancerek (Bialystok Technical University) 
17.50  A declarative proof mode for Coq 

Pierre Corbineau (Radboud Universiteit Nijmegen) 


18.00  Close 


19.15  Bus to Banquet from Newark Hall 


19.30  TYPES and TFP Conference Banquet at Mem Saab, Maid Marian Way 


22.30  Bus from Banquet from Mem Saab 



07.30  Breakfast in the Catering Facility 


09.00  System F with TypeEquality Coercions (invited talk) 

Simon Peyton Jones (Microsoft Research) 


10.00  Coffee 


10.30  Dependent Type Theory for State and Aliasing 

Aleksandar Nanevski (Harvard University) 
10.55  Intersection Types for Costanalysis of Functional Programs 

Hugo Simoes (University of St Andrews) 
11.20  Enhancing Elementary Affine Logic Type Inference with Implicit Coercions 

Vincent Atassi (LIPN, Université Paris 13) 
11.45  Computation by Prophecy 

Venanzio Capretta (University of Ottawa) 


12.10  Lunch in the Catering Facility 


14.00  Verification of Programs with Truly Nested Datatypes in Coq 

Ralph Matthes (IRIT, Toulouse) 
14.25  Certifying the Implementation of a Distributed Security Logic using Coq 

Nathan Whitehead (University of California, Santa Cruz) 
14.50  Global Formal Optimization Using Taylor Models 

Roland Zumkeller (LIX  Ecole Polytechnique) 
15.15  Formal Proof of Petri Net Refinement using Coq 

Micaela Mayero (LIPN, Université Paris 13) 


15.40  Coffee 


16.00  Verification in Coq of Iteration Schemes for Nested Datatypes 

Dulma Rodriguez (LudwigMaximiliansUniversität, München) 
16.10  Strictly Positive Families 

Peter Morris (University of Nottingham) 
16.20  An Algebra of Dependent Data Types 

TyngRuey Chuang (Academia Sinica, Taiwan) 
16.30  Algebra of Dependent Types 

Andrzej Trybulec (University of Bialystok) 
16.40  Semantic Normalisation Proofs 

Ulrich Berger (Prifysgol Cymru Abertawe) 


16.50  Break 


17.00  Type Systems for Resource Use of Component Software 

Hoang Anh Truong (University of Bergen) 
17.10  Testing using Dependent Types 

Fredrik Lindblad (Chalmers University of Technology) 
17.20  A Dependently Typed Framework for Maintaining Invariants 

Lazlo Nemeth (Istanbul Bilgi University) 
17.30  Towards Intensionally More Expressive Systems for PTIME 

Stefan Schimanski (LudwigMaximiliansUniversität, München) 
17.40  On the Density of Types with Decidable λDefinability Problem 

Marek Zaionc (Jagiellonian University) 
17.50  Types and Layered Logics for Program Verification 

Olha Shkaravska (Institute of Cybernetics, Tallinn) 


18.00  Close 


18.30  Dinner in the Catering Facility 


20.00  Business Meeting 





07.30  Breakfast in the Catering Facility 
09.00  Functional Extraction of Inductive Predicates 

David Delahaye (CNAM, CEDRIC  LogiCal) 
09.25  A Solution to the POPLmark Challenge in Isabelle/HOL 

Stefan Berghofer (Technische Universität München) 
09.50  Subset Coercions in Coq 

Matthieu Sozeau (LRI, Université ParisSud) 
10.15  Subset Types in a Proof Irrelevant Type Theory 

Benjamin Werner (LIX  INRIA Futurs) 


10.40  Coffee 


11.00  CoverTranslatorfrom Haskell to First Order Logic 

Patrik Jansson (Chalmers University of Technology) 
11.25  Defining Partial Recursive Functions in Isabelle/HOL 

Alexander Krauss (Technische Universität München) 
11.50  Constrained Based Termination 

Colin Riba (INRIA  LORIA) 
12.15  HigherOrder Subtyping Revisited 

Andreas Abel (LudwigMaximiliansUniversität, München) 


12.40  Lunch in the Catering Facility 
