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 (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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
|
|
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 |
|