About Conferences Colloquium Workshops Practical

TLCA 2007 Programme



Tuesday, June 26


8:15 - 9:00      Arrival of participants and registration

       RTA/TLCA joint invited speaker (Amphithéâtre Jean Fourastié)
    Chair: Femke van Raamsdonk
8:55 - 9:00      Welcome.
9:00 - 10.00      Frank Pfenning. On a Logical Foundation for Explicit Substitutions.

10:00 - 10:30      Coffee Break

       TLCA Session 2 (Amphithéâtre Jean Prouvé)
    Chair: Paula Severi
10:30 - 11:00      Marcelo Fiore. Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic.
11:00 - 11:30      Ying Jiang and Guo-Qiang Zhang. Weakly Distributive Domains.
11:30 - 12:00      Neil Ghani and Patricia Johann. Initial Algebra Semantics is Enough!
12:00 - 12:30      William Blum and Luke Ong. The Safe Lambda Calculus.

12:30 - 14:00      Lunch

       TLCA Session 3 (Amphithéâtre Jean Prouvé)
    Chair: Pawel Urzyczyn
14:00 - 14:30      Benedetto Intrigila and Richard Statman. The Omega Rule is Π11 Complete in the Lambda-Calculus.
14:30 - 15:00      Sam Lindley. Extensional rewriting with sums.

15:30 - 16:00      Coffee Break

       TLCA Session 4 (Amphithéâtre Jean Prouvé)
    Chair: Simone Martini
15:30 - 16:00      Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction.
16:00 - 16:30      Jose Espirito Santo. Completing Herbelin's Programme.
16:30 - 17:00      Jose Espirito Santo, Ralph Matthes and Luís Pinto. Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi.

       TLCA business meeting (Amphithéâtre Jean Prouvé)
17:10 - 18:00      TLCA business meeting.

       RDP Reception (Chapel)
18:00 - 22:00      Reception, with an evening talk by Henk Barendregt. The Diamond Anniversary of Lambda Calculus.

Wednesday, June 27


8:15 - 9:00      Arrival of participants

       RTA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Manfred Schmidt-Schauß
9:00 - 10.00      Xavier Leroy. Formal Verification of an Optimizing Compiler.

10:00 - 10:30      Coffee Break

       TLCA Session 6 (Amphithéâtre Jean Prouvé)
    Chair: Healf Goguen
10:30 - 11:00      Makoto Tatsuta. Simple saturated sets for disjunction and second-order existential quantification.
11:00 - 11:30      René David and Karim Nour. An arithmetical proof of the strong normalization for the lambda-calculus with recursive equations on types.
11:30 - 12:00      Andreas Abel. Strong Normalization and Equi-(co)inductive Types.
12:00 - 12:30      Dariusz Kusmierek. The inhabitation problem for rank two intersection types.

12:30 - 14:00      Lunch

       TLCA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Frank Pfenning
14:00 - 15:00      Greg Morrisett. The Marriage of Dependent Types and Effects.

15:00 - 15:30      Coffee Break

       TLCA Session 8 (Amphithéâtre Jean Prouvé)
    Chair: Peter Dybjer
15:30 - 16:00      Sylvain Boulmé. Intuitionistic Refinement Calculus.
16:00 - 16:30      Oleg Kiselyov and Chung-chieh Shan. A Substructural Type System for Delimited Continuations.
16:30 - 17:00      Ana Bove and Venanzio Capretta. Computation by Prophecy.
17:00 - 17:30      Denis Cousineau and Gilles Dowek. Embedding Pure Type Systems in the lambda Pi calculus modulo.

       RDP business meetings (Amphithéâtre Friedmann)
17:45 - 18:15      RDP business meeting.

21:00 - 23:00      RDP Banquet

Thursday, June 28


8:15 - 9:00      Arrival of participants

       TLCA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Simona Ronchi Della Rocca
9:00 - 10.00      Patrick Baillot. From Proof-Nets to linear Logic Type Systems for Polynomial Time Computing.

10:00 - 10:30      Coffee Break

       TLCA Session 10 (Amphithéâtre Jean Prouvé)
    Chair: Patrick Baillot
10:30 - 11:00      Jean-Yves Marion. Predicative analysis of feasibility and diagonalisation.
11:00 - 11:30      Olha Shkaravska, Ron van Kesteren and Marko van Eekelen. Polynomial Size Analysis of First-Order Functions.
11:30 - 12:00      Stefano Berardi. An Semantic for Intuitionistic Arithmetic based on Tarski Games.
12:00 - 12:30      James Lipton and Susana Nieva. Higher Order Logic Programming Languages with Constraints: a Semantics.

12:30 - 14:00      Lunch

       RTA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Franz Baader
14:00 - 15:00      Robert Nieuwenhuis. Challenges in Satisfiability Modulo Theories.

15:00 - 15:30      Coffee Break

       TLCA Session 12 (Amphithéâtre Jean Prouvé)
    Chair: Olivier Laurent
15:30 - 16:00      Damiano Mazza. Edifices: Boehm Trees for the Interaction Combinators.
16:00 - 16:30      Claudia Faggian and Mauro Piccolo. Ludics is a model for the (finitary) linear Pi-calculus.
16:30 - 17:00      Dimitris Mostrous and Nobuko Yoshida. Two Session Typing Systems for Higher-Order Mobile Processes.
17:00 - 17:30      Lionel Vaux. Convolution lambda-bar-mu-calculus.

webmaster at rdp07 dot org