Ebook: 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.

---

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.

---

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.
Content:
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 -

---

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.
Content:
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 -
....