RDP 2013, Eindhoven: RTA + TLCA

Conference Programme

You may also consider the full program in PDF, including the workshop programs

Sunday 23 June 2013

17:00-19:00 Opening reception in Zwarte Doos

Monday 24 June 2013

RTA Session 1 (Room 7)

09:00-09:05 opening
09:05-10:05 Jarkko Kari (invited talk) Pattern Generation by Cellular Automata

RTA Session 2 (Room 7)

10:30-11:00 Christian Sternagel and René Thiemann Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
11:00-11:30 Sarah Winkler and Aart Middeldorp Normalized Completion Revisited
11:30-12:00 Anupam Das Rewriting with linear inferences in propositional logic

RTA Session 3 (Room 7)

14:00-14:30 Alexander Baumgartner, Temur Kutsia, Jordi Levy and Mateu Villaret A Variant of Higher-Order Anti-Unification
14:30-15:00 Christophe François Olivier Calvès Unifying Nominal Unification
15:00-15:30 Gert Smolka and Tobias Tebbi Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification


14:00-17:00 COS: Control Operators and their Semantics, Room 12

RTA Session 4 (Room 7)

16:00-16:30 Beniamino Accattoli Linear logic and strong normalization
16:30-17:00 Yves Guiraud, Philippe Malbos and Samuel Mimram A Homotopical Completion Procedure with Applications to Coherence of Monoids

Tuesday 25 June 2013

RTA Session 5 (Room 7)

09:00-10:00 Mitsu Okada (invited talk) Husserl and Hilbert on Completeness and Husserl's Term Rewrite-based Theory of Multiplicity


9:00-17:00 COS: Control Operators and their Semantics, Room 12

RTA Session 6 (Room 7)

10:30-11:00 Bertram Felgenhauer and Vincent van Oostrom Proof Orders for Decreasing Diagrams
11:00-11:30 Harald Zankl Confluence by Decreasing Diagrams Formalized
11:30-12:00 Yohan Boichut, Chabin Jacques and Pierre Rety Over-approximating Descendants by Synchronized Tree Languages

RTA Session 7 (Room 7)

14:00-14:30 Manfred Schmidt-Schauß, Elena Machkasova and David Sabel Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings
14:30-15:00 Clemens Grabmayer and Jan Rochel Expressibility in the Lambda Calculus with Mu
15:00-15:30 Ken-Etsu Fujita and Aleksy Schubert Decidable structures between Church-style and Curry-style

RTA Session 8 (Room 7)

16:00-16:30 Kyungmin Bae, Santiago Escobar and Jose Meseguer Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
16:30-17:00 Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti and Olga Kouchnarenko Automatic Decidability: A Schematic Calculus for Theories with Counting Operators

17:00-... RTA business meeting (Room 7)

Wednesday 26 June 2013

RTA Session 9 = TLCA Session 1 (Room 7)

09:00-10:00 Simon Peyton-Jones (joint invited talk) Type-Directed Compilation in the Wild: Haskell and Core

RTA Session 10 (Room 7)

10:30-11:00 Manfred Schmidt-Schauß, Conrad Rau and David Sabel Algorithms for Alpha-Equivalence and Complexity
11:00-11:30 Martin Avanzini and Georg Moser A Combination Framework for Complexity
11:30-12:00 Alexander Bau, Markus Lohrey, Eric Noeth and Johannes Waldmann Compression of Rewriting Systems for Termination Analysis

TLCA Session 2 (Room 8)

10:25-10:30 TLCA Opening and Welcome
10:30-11:00 Ki Yung Ahn, Tim Sheard, Marcelo Fiore and Andrew Pitts System Fi: a Higher-Order Polymorphic Lambda Calculus with Erasable Term-Indices
11:00-11:30 Nick Benton, Martin Hofmann and Vivek Nigam Proof-Relevant Logical Relations for Name Generation
11:30-12:00 Paula Severi and Fer-Jan de Vries Completeness of Conversion between Reactive Programs for Ultrametric Models

RTA Session 11 (Room 7)

14:00-14:30 Sarah Winkler, Harald Zankl and Aart Middeldorp Beyond Peano Arithmetic Automatically Proving Termination of the Goodstein Sequence
14:30-15:00 Martin Avanzini and Georg Moser Tyrolean Complexity Tool: Features and Usage
15:00-15:30 René Thiemann Termination Competition

TLCA Session 3 (Room 8)

14:00-14:30 Daniel Fridlender and Miguel Pagano A Type-Checking Algorithm for Martin-Loef Type Theory with Subtyping Based on Normalisation by Evaluation
14:30-15:00 Boris Duedder Moritz Martens and Jakob Rehof Intersection Type Matching with Subtyping
15:00-15:15 Henk Barendregt About "Lambda Calculus with Types"
15:15-15:30 Pawel Urzyczyn On TLCA List of Open Problems

17:00- Excursion, Conference Dinner (DAF museum)

Thursday 27 June 2013


9:00-12:00 IFIP WG 1.6: IFIP Working Group 1.6 on Term Rewriting, Room 12a
9:00-17:00 UNIF: International Workshop on Unification, Room 12b
14:00-17:00 HART: Haskell And Rewriting Techniques, Room 12a

TLCA Session 4 (Room 7)

09:00-10:00 Hugo Herbelin (invited talk) Proving with Side-Effects

TLCA Session 5 (Room 7)

10:30-11:00 Stefano Berardi and Makoto Tatsuta Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics
11:00-11:30 Valentin Blot Realizability for Peano Arithmetic with Winning Conditions in HO Games
11:30-12:00 Ulrich Schoepp On Interaction, Continuations and Defunctionalization

TLCA Session 6 (Room 7)

14:30-15:00 Federico Aschieri and Margherita Zorzi Non-Determinism and the Strong Normalization of System T
15:00-15:30 Pierre Clairambault Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction

TLCA Session 7 (Room 7)

16:00-16:30 Sylvain Salvati and Igor Walukiewicz Using Models to Model-check Recursive Schemes
16:30-17:00 Flavien Breuvart The Resource Lambda Calculus is Short-Sighted in Its Relational Model

17:30-... TLCA Business Meeting (Room 7)

Friday 28 June 2013


9:00-12:10 IWC: International Workshop on Confluence, Room 12a
9:00-12:00 WIR: Workshop on Infinitary Rewriting, Room 12b
14:00-14:45 Jan Willem Klop (joint IWC/WIR invited talk) Confluence and Infinity - a kaleidoscopic view (Room 7)
15:00-17:45 IWC: International Workshop on Confluence, Room 7
15:30-16:30 WIR: Workshop on Infinitary Rewriting, Room 12b

TLCA Session 8 (Room 7)

09:00-10:00 Damiano Mazza (invited talk) Non-Linearity as the Metric Completion of Linearity

TLCA Session 9 (Room 7)

10:30-11:00 Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta and Thorsten Altenkirch Small Induction Recursion
11:00-11:30 Nicolai Kraus, Martin Escardo, Thierry Coquand and Thorsten Altenkirch Generalizations of Hedberg's Theorem
11:30-12:00 Chuangjie Xu and Martin Escardo A Constructive Model of Uniform Continuity
12:00-12:10 Closing