Typed lambda calculi and applications : 11th International Conference, TLCA 2013, Eindhoven, the Netherlands, June 26-28, 2013 : proceedings

This book constitutes the refereed proceedings of the 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013, held in Eindhoven, The Netherlands, in June 2013 as part of RDP 2013, the 7th Federated Conference on Rewriting, Deduction, and Programming, together with the 24th International Conference on Rewriting Techniques and Applications, RTA 2013, and several related events. The 15 revised full papers presented were carefully reviewed and selected from 41 submissions. The papers provide prevailing research results on all current aspects of typed lambda calculi, ranging from theoretical and methodological issues to applications in various contexts addressing a wide variety of topics such as proof-theory, semantics, implementation, types, and programming. Front Matter....Pages - Type-Directed Compilation in the Wild: Haskell and Core....Pages 1-1 Proving with Side Effects....Pages 2-2 Non-linearity as the Metric Completion of Linearity....Pages 3-14 System F i ....Pages 15-30 Non-determinism, Non-termination and the Strong Normalization of System T....Pages 31-47 Proof-Relevant Logical Relations for Name Generation....Pages 48-60 Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics....Pages 61-76 Realizability for Peano Arithmetic with Winning Conditions in HON Games....Pages 77-92 The Resource Lambda Calculus Is Short-Sighted in Its Relational Model....Pages 93-108 Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction....Pages 109-124 Intersection Type Matching with Subtyping....Pages 125-139 A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation....Pages 140-155 Small Induction Recursion....Pages 156-172 Generalizations of Hedberg’s Theorem....Pages 173-188 Using Models to Model-Check Recursive Schemes....Pages 189-204 On Interaction, Continuations and Defunctionalization....Pages 205-220 Completeness of Conversion between Reactive Programs for Ultrametric Models....Pages 221-235 A Constructive Model of Uniform Continuity....Pages 236-249 Back Matter....Pages -