8. TLCA 2007: Paris, France

• Frank Pfenning:
  On a Logical Foundation for Explicit Substitutions. 1
  Electronic Edition (link) BibTeX
• Patrick Baillot:
  From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing. 2-7
  Electronic Edition (link) BibTeX
• Andreas Abel:
  Strong Normalization and Equi-(Co)Inductive Types. 8-22
  Electronic Edition (link) BibTeX
• Stefano Berardi:
  Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves. 23-38
  Electronic Edition (link) BibTeX
• William Blum, C.-H. Luke Ong:
  The Safe Lambda Calculus. 39-53
  Electronic Edition (link) BibTeX
• Sylvain Boulmé:
  Intuitionistic Refinement Calculus. 54-69
  Electronic Edition (link) BibTeX
• Ana Bove, Venanzio Capretta:
  Computation by Prophecy. 70-83
  Electronic Edition (link) BibTeX
• René David, Karim Nour:
  An Arithmetical Proof of the Strong Normalization for the lambda -Calculus with Recursive Equations on Types. 84-101
  Electronic Edition (link) BibTeX
• Denis Cousineau, Gilles Dowek:
  Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. 102-117
  Electronic Edition (link) BibTeX
• José Espírito Santo:
  Completing Herbelin's Programme. 118-132
  Electronic Edition (link) BibTeX
• José Espírito Santo, Ralph Matthes, Luis Pinto:
  Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi. 133-147
  Electronic Edition (link) BibTeX
• Claudia Faggian, Mauro Piccolo:
  Ludics is a Model for the Finitary Linear Pi-Calculus. 148-162
  Electronic Edition (link) BibTeX
• Marcelo P. Fiore:
  Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic. 163-177
  Electronic Edition (link) BibTeX
• Benedetto Intrigila, Richard Statman:
  The Omega Rule is P₁¹-Complete in the lambdabeta -Calculus. 178-193
  Electronic Edition (link) BibTeX
• Ying Jiang, Guo-Qiang Zhang:
  Weakly Distributive Domains. 194-206
  Electronic Edition (link) BibTeX
• Patricia Johann, Neil Ghani:
  Initial Algebra Semantics Is Enough! 207-222
  Electronic Edition (link) BibTeX
• Oleg Kiselyov, Chung-chieh Shan:
  A Substructural Type System for Delimited Continuations. 223-239
  Electronic Edition (link) BibTeX
• Dariusz Kusmierek:
  The Inhabitation Problem for Rank Two Intersection Types. 240-254
  Electronic Edition (link) BibTeX
• Sam Lindley:
  Extensional Rewriting with Sums. 255-271
  Electronic Edition (link) BibTeX
• James Lipton, Susana Nieva:
  Higher-Order Logic Programming Languages with Constraints: A Semantics. 272-289
  Electronic Edition (link) BibTeX
• Jean-Yves Marion:
  Predicative Analysis of Feasibility and Diagonalization. 290-304
  Electronic Edition (link) BibTeX
• Damiano Mazza:
  Edifices and Full Abstraction for the Symmetric Interaction Combinators. 305-320
  Electronic Edition (link) BibTeX
• Dimitris Mostrous, Nobuko Yoshida:
  Two Session Typing Systems for Higher-Order Mobile Processes. 321-335
  Electronic Edition (link) BibTeX
• Koji Nakazawa:
  An Isomorphism Between Cut-Elimination Procedure and Proof Reduction. 336-350
  Electronic Edition (link) BibTeX
• Olha Shkaravska, Ron van Kesteren, Marko C. J. D. van Eekelen:
  Polynomial Size Analysis of First-Order Functions. 351-365
  Electronic Edition (link) BibTeX
• Makoto Tatsuta:
  Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. 366-380
  Electronic Edition (link) BibTeX
• Lionel Vaux:
  Convolution [`(l)]m-Calculus. 381-395
  Electronic Edition (link) BibTeX