Programme for TLCA 2009

Wednesday, July 1

Sessions 1 and 2 (chaired by Pierre-Louis Curien)

 09:00-10:00  Joint Invited Talk:  Robert Harper. A pronominal approach to binding and computation

10:30-11:00 Andreas Abel, Thierry Coquand and Miguel Pagano. A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

11:00-11:30 Gunnar Wilken and Andreas Weiermann. Complexity of G\"odel's $\mathrm{T}$ in $\lambda$-Formulation

11:30-12:00 William Lovas and Frank Pfenning. Refinement Types as Proof Irrelevance

Session 3  (chaired by Jonathan Seldin)

14:00-14:30 Ken-etsu Fujita and Aleksy Schubert. Existential type systems with no types in terms

14:30-15:00 Takeshi Tsukada and Atsushi Igarashi. A Logical Foundation for Environment Classifiers

15:00-15:30 Pawel Urzyczyn. Inhabitation of low-rank intersection  types

Session 4 (chaired by Jean-Pierre Jouannaud)

16:00-16:30 Colin Riba. On the Values of Reducibility Candidates

16:30-17:00 Barbara Petit. A polymorphic type system for lambda-calculus with constructors

17:00-17:30 Hugo Herbelin and Stéphane Zimmermann. An operational account of call-by-value minimal and classical lambda-calculus in "natural deduction" form

17:30-18:00 Jeffrey Sarnat and Carsten Schuermann. Lexicographic Path Induction

Thursday, July 2

Sessions 5  and 6 (chaired by Luca Paolini)

 09:00-10:00 Invited Talk: Jean-Louis Krivine. Ultrafilters and the heap

10:30-11:00 Claudia Faggian. Partial Orders, Event Structures, and Linear Strategies

11:00-11:30 Pierre Boudes. Thick Subtrees, Games and Experiments

11:30-12:00 Michele Basaldella and Kazushige Terui. On the meaning of logical completeness

Session 7  (chaired by Robert Harper)

14:00-14:30 Robert Atkey. Syntax For Free: Representing Syntax with Binding using Parametricity

14:30-15:00 Florian Stenger and Janis Voigtländer. Parametricity for Haskell with Imprecise Error Semantics

15:00-15:30 Dimitris Mostrous and Nobuko Yoshida. Session-based Communication Optimisation for Higher-Order Mobile Processes

Session 8 (chaired by Pawel Urzyczyn)

16:00-16:30  Florian Rabe and Steve Awodey. Kripke Semantics for Martin-Loef Type Theory

16:30-17:00 Peter LeFanu Lumsdaine. Weak omega-categories from intensional type theory

17:00-17:30 Federico Aschieri and Stefano Berardi. A Realizability Interpretation for Heyting Arithmetic with Excluded Middle over Sigma-0-1 formulas

17:30-18:00 Alexandre Miquel. Relating classical realizability and negative translation for existential witness extraction.

 Friday, July 3

Sessions 9 and 10  (chaired by Elaine Pimentel)

09:00-10:00 Invited Talk: Marcelo Fiore. Mathematical synthesis of equational deduction systems

10:30-11:00 Christine Tasson. Algebraic totality, towards completeness.

11:00-11:30 Yu Zhang. The computational SLR: a logic for reasoning about computational indistinguishability

11:30-12:00 Makoto Hamana. Initial Algebra Semantics for Cyclic Sharing Structures

Session 11  (chaired by Marcelo Fiore)

14:00-14:30  Lutz Strassburger. Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic

14:30-15:00 Lionel Vaux. Differential Linear Logic and Polarization

15:00-15:30  Ugo Dal Lago and Martin Hofmann. Bounded Linear Logic, Revisited

15:30-16:00 Michele Pagani. The Cut-Elimination Theorem for Differential Nets with boxes

Session 12

16:30-17:30 TLCA Bussiness Meeting