Typed Lambda Calculi and Applications : 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009, Proceedings

This book constitutes the refereed proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009, held in Brasilia, Brazil in July 2008 in conjunction with RTA 2007, the 19th International Conference on Rewriting Techniques and Applications as part of RDP 2009, the 5th International Conference on Rewriting, Deduction, and Programming. The 27 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 53 submissions. The papers present original research results that are broadly relevant to the theory and applications of typed calculi and address a wide variety of topics such as proof-theory, semantics, implementation, types, and programming. Front Matter....Pages - Mathematical Synthesis of Equational Deduction Systems....Pages 1-2 A Pronominal Approach to Binding and Computation....Pages 3-4 A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance....Pages 5-19 Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1 ....Pages 20-34 Syntax for Free: Representing Syntax with Binding Using Parametricity....Pages 35-49 On the Meaning of Logical Completeness....Pages 50-64 Thick Subtrees, Games and Experiments....Pages 65-79 Bounded Linear Logic, Revisited....Pages 80-94 Partial Orders, Event Structures and Linear Strategies....Pages 95-111 Existential Type Systems with No Types in Terms....Pages 112-126 Initial Algebra Semantics for Cyclic Sharing Structures....Pages 127-141 An Operational Account of Call-by-Value Minimal and Classical λ -Calculus in “Natural Deduction” Form....Pages 142-156 Refinement Types as Proof Irrelevance....Pages 157-171 Weak ω -Categories from Intensional Type Theory....Pages 172-187 Relating Classical Realizability and Negative Translation for Existential Witness Extraction....Pages 188-202 Session-Based Communication Optimisation for Higher-Order Mobile Processes....Pages 203-218 The Cut-Elimination Theorem for Differential Nets with Promotion....Pages 219-233 A Polymorphic Type System for the Lambda-Calculus with Constructors....Pages 234-248 Kripke Semantics for Martin-Löf’s Extensional Type Theory....Pages 249-263 On the Values of Reducibility Candidates....Pages 264-278 Lexicographic Path Induction....Pages 279-293 Parametricity for Haskell with Imprecise Error Semantics....Pages 294-308 Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic....Pages 309-324 Algebraic Totality, towards Completeness....Pages 325-340 A Logical Foundation for Environment Classifiers....Pages 341-355 Inhabitation of Low-Rank Intersection Types....Pages 356-370 Differential Linear Logic and Polarization....Pages 371-385 Complexity of Gödel’s T in λ -Formulation....Pages 386-400 The Computational SLR: A Logic for Reasoning about Computational Indistinguishability....Pages 401-415 Back Matter....Pages -