Rewriting and Typed Lambda Calculi

1. Front Matter

   PDF

2. Process Types as a Descriptive Tool for Interaction

   • Kohei Honda, Nobuko Yoshida, Martin Berger

   Pages 1-20

3. Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk)

   • Manfred Schmidt-Schauß

   Pages 21-30

4. Unnesting of Copatterns

   • Anton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau

   Pages 31-45

5. Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams

   • Takahito Aoto, Yoshihito Toyama, Kazumasa Uchida

   Pages 46-60

6. Predicate Abstraction of Rewrite Theories

   • Kyungmin Bae, José Meseguer

   Pages 61-76

7. Unification and Logarithmic Space

   • Clément Aubert, Marc Bagnol

   Pages 77-92

8. Ramsey Theorem as an Intuitionistic Property of Well Founded Relations

   • Stefano Berardi, Silvia Steila

   Pages 93-107

9. A Model of Countable Nondeterminism in Guarded Type Theory

   • Aleš Bizjak, Lars Birkedal, Marino Miculan

   Pages 108-123

10. Cut Admissibility by Saturation

    • Guillaume Burel

    Pages 124-138

11. Automatic Evaluation of Context-Free Grammars (System Description)

    • Carles Creus, Guillem Godoy

    Pages 139-148

12. Tree Automata with Height Constraints between Brothers

    • Carles Creus, Guillem Godoy

    Pages 149-163

13. A Coinductive Confluence Proof for Infinitary Lambda-Calculus

    • Łukasz Czajka

    Pages 164-178

14. An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting

    • Daniel de Carvalho, Jakob Grue Simonsen

    Pages 179-193

15. Preciseness of Subtyping on Intersection and Union Types

    • Mariangiola Dezani-Ciancaglini, Silvia Ghilezan

    Pages 194-207

16. Abstract Datatypes for Real Numbers in Type Theory

    • Martín Hötzel Escardó, Alex Simpson

    Pages 208-223

17. Self Types for Dependently Typed Lambda Encodings

    • Peng Fu, Aaron Stump

    Pages 224-239

18. First-Order Formative Rules

    • Carsten Fuhs, Cynthia Kop

    Pages 240-256

19. Automated Complexity Analysis Based on Context-Sensitive Rewriting

    • Nao Hirokawa, Georg Moser

    Pages 257-271

20. Amortised Resource Analysis and Typed Polynomial Interpretations

    • Martin Hofmann, Georg Moser

    Pages 272-286

This book constitutes the refereed proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications, RTA 2014, and 12th International Conference on Typed Lambda-Calculi and Applications, TLCA 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 28 revised full papers and 3 short papers presented were carefully reviewed and selected from 87 submissions. The papers provide research results on all aspects of rewriting and typed lambda calculi, ranging from theoretical and methodological issues to applications in various contexts. They address a wide variety of topics such as algorithmic aspects, implementation, logic, types, semantics, and programming.

• automata
• complexity analysis
• constraint and logic programming
• constructive mathematics
• lambda-mu calculus
• logic
• model checking
• pattern matching
• proof theory
• type theory

• Inria, Paris Cedex 13, France

  Gilles Dowek

Policies and ethics