9. TLCA 2009: Brasilia, Brazil

• Marcelo P. Fiore, Chung-Kil Hur:
  Mathematical Synthesis of Equational Deduction Systems. 1-2
  
• Robert Harper, Daniel R. Licata, Noam Zeilberger:
  A Pronominal Approach to Binding and Computation. 3-4
  
• Andreas Abel, Thierry Coquand, Miguel Pagano:
  A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. 5-19
  
• Federico Aschieri, Stefano Berardi:
  Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. 20-34
  
• Robert Atkey:
  Syntax for Free: Representing Syntax with Binding Using Parametricity. 35-49
  
• Michele Basaldella, Kazushige Terui:
  On the Meaning of Logical Completeness. 50-64
  
• Pierre Boudes:
  Thick Subtrees, Games and Experiments. 65-79
  
• Ugo Dal Lago, Martin Hofmann:
  Bounded Linear Logic, Revisited. 80-94
  
• Claudia Faggian, Mauro Piccolo:
  Partial Orders, Event Structures and Linear Strategies. 95-111
  
• Ken-etsu Fujita, Aleksy Schubert:
  Existential Type Systems with No Types in Terms. 112-126
  
• Makoto Hamana:
  Initial Algebra Semantics for Cyclic Sharing Structures. 127-141
  
• Hugo Herbelin, Stéphane Zimmermann:
  An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. 142-156
  
• William Lovas, Frank Pfenning:
  Refinement Types as Proof Irrelevance. 157-171
  
• Peter LeFanu Lumsdaine:
  Weak omega-Categories from Intensional Type Theory. 172-187
  
• Alexandre Miquel:
  Relating Classical Realizability and Negative Translation for Existential Witness Extraction. 188-202
  
• Dimitris Mostrous, Nobuko Yoshida:
  Session-Based Communication Optimisation for Higher-Order Mobile Processes. 203-218
  
• Michele Pagani:
  The Cut-Elimination Theorem for Differential Nets with Promotion. 219-233
  
• Barbara Petit:
  A Polymorphic Type System for the Lambda-Calculus with Constructors. 234-248
  
• Steven Awodey, Florian Rabe:
  Kripke Semantics for Martin-Löf's Extensional Type Theory. 249-263
  
• Colin Riba:
  On the Values of Reducibility Candidates. 264-278
  
• Jeffrey Sarnat, Carsten Schürmann:
  Lexicographic Path Induction. 279-293
  
• Florian Stenger, Janis Voigtländer:
  Parametricity for Haskell with Imprecise Error Semantics. 294-308
  
• Lutz Straßburger:
  Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic. 309-324
  
• Christine Tasson:
  Algebraic Totality, towards Completeness. 325-340
  
• Takeshi Tsukada, Atsushi Igarashi:
  A Logical Foundation for Environment Classifiers. 341-355
  
• Pawel Urzyczyn:
  Inhabitation of Low-Rank Intersection Types. 356-370
  
• Lionel Vaux:
  Differential Linear Logic and Polarization. 371-385
  
• Gunnar Wilken, Andreas Weiermann:
  Complexity of Gödel's T in lambda-Formulation. 386-400
  
• Yu Zhang:
  The Computational SLR: A Logic for Reasoning about Computational Indistinguishability. 401-415