--> -->

TYPES 2006

University of Nottingham, UK, 18 - 21 April, 2006



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.

Monday 17 April

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

21.00 Close

Tuesday 18 April

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 (Ludwig-Maximilians-Universitä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 Walukiewicz-Chraszcz (Warsaw University)
16.20  Dependent Type Theory with Pattern-Matching and Size-Change Termination

   David Wahlstedt (Chalmers University of Technology)
16.30  A Practical Approach to Co-induction 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 cut-elimination

   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  Multi-Level Lax Logic

   Mike Stannett (University of Sheffield)

18.00 Close

18.30 Dinner in the Catering Facility

Wednesday 19 April

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 Meta-programming (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 Xor-Terms (TFP talk)

   Jean-Franç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

   Claudio-Sacerdoti Coen + Enrico Tassi (Università di Bologna)

15.40 Coffee

16.00  Representation of partial recursive functions by inductive-recursive 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 context-free 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 Proof-Search

   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

Thursday 20 April

07.30 Breakfast in the Catering Facility

09.00  System F with Type-Equality 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 Cost-analysis 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 (Ludwig-Maximilians-Universität, München)
16.10  Strictly Positive Families

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

   Tyng-Ruey 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 (Ludwig-Maximilians-Universitä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

Friday 21 April

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é Paris-Sud)
10.15  Subset Types in a Proof Irrelevant Type Theory

   Benjamin Werner (LIX - INRIA Futurs)

10.40 Coffee

11.00  CoverTranslator---from 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  Higher-Order Subtyping Revisited

   Andreas Abel (Ludwig-Maximilians-Universität, München)

12.40 Lunch in the Catering Facility