RDP Programme

Monday, May 30th

09:00-09:30 RTA Opening and Welcome

Coffee Break (09:30-10:00)

Session 1 (10:00-11:00)

Chair: Manfred Schmidt-Schauß

10:00-11:00 Invited talk: Sophie Tison. Tree Automata, (Dis-)Equality Constraints and Term Rewriting: What's New?.

Session 2 (11:00-12:20)

Chair: Georg Moser

11:00-11:30 Paula Severi and Fer-Jan de Vries. Weakening the Axiom of Overlap in Infinitary Lambda Calculus.

11:30-12:00 Patrick Bahr. Modes of Convergence for Term Graph Rewriting.

12:00-12:20 Niels Bjørn Bugge Grathwohl, Jeroen Ketema, Jens Duelund Pallesen, and Jakob Grue Simonsen. Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus.

Lunch Break (12:20-14:15)

Session 3 (14:15-15:55)

Chair: Johannes Waldmann

14:15-14:45 Marc Brockschmidt, Carsten Otto, and Jürgen Giesl. Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting.

14:45-15:15 Christian Sternagel and René Thiemann. Modular and Certified Semantic Labeling and Unlabeling.

15:15-15:30 Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3.

15:35-15:55 Stephan Falke, Deepak Kapur, and Carsten Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages.

Coffee Break (15:55-16:15)

Session 4 (16:15-18:15)

Chair: Jürgen Giesl

16:15-16:45 Cynthia Kop and Femke van Raamsdonk. Higher Order Dependency Pairs for Algebraic Functional Systems.

16:45-17:15 Cody Roux. Refinement Types as Higher-Order Dependency Pairs.

17:15-18:45 Georg Moser and Andreas Schnabl. Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity.

17:45-18:15 Friedrich Neurauter and Aart Middeldorp. Revisiting Matrix Interpretations for Proving Termination of Term Rewriting.

Tuesday, May 31st

Session 5 (09:00-10:00)

Chair: Narciso Marti-Oliet

09:00-10:00 Invited talk: Ashish Tiwari. Rewriting in Practice.

Coffee Break (10:00-10:30)

Session 6 (10:30-11:50)

Chair: Ren'e Thiemann

10:30-11:00 Hans Zantema and Jörg Endrullis. Proving Equality of Streams Automatically.

11:00-11:30 Naoki Nishida and Germán Vidal. Program Inversion for Tail Recursive Functions.

11:30-11:50 Kristoffer H. Rose. CRSX - Combinatory Reduction Systems with Extensions.

Lunch Break (11:50-14:00)

Session 7 (14:00-15:40)

Chair: Hans Zantema

14:00-14:30 Aaron Stump, Garrin Kimmell, and Roba El Haj Omar. Type Preservation as a Confluence Problem.

14:30-15:00 Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. Labelings for Decreasing Diagrams.

15:00-15:20 Dominik Klein and Nao Hirokawa. Maximal Completion.

15:20-15:40 Bruno Conchinha, David Basin, and Carlos Caleiro. FAST: An Efficient Decision Procedure for Deduction and Static Equivalence.

Coffee Break (15:40-16:10)

Session 8 (16:10-17:40)

Chair: Manfred Schmidt-Schauß

16:10-16:30 Adrià Gascón, Sebastian Maneth, and Lander Ramos. First-Order Unification on Compressed Terms.

16:30-16:50 Francisco Durán, Steven Eker, Santiago Escobar, José Meseguer, and Carolyn Talcott. Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6.

16:50-17:20 Temur Kutsia, Jordi Levy, and Mateu Villaret. Anti-Unification for Unranked Terms and Hedges.

17:20-17:40 Irène Durand and Marc Sylvestre. Left-linear Bounded TRSs are Inverse Recognizability Preserving.

Coffee Break (17:40-18:00)

RTA Business Meeting (18:00-19:00)

18:00-19:00 RTA Business Meeting.

Wednesday, June 1st

Session 9 (09:00-10:00)

Chair: Luke Ong

09:00-10:00 Invited talk: Stephanie Weirich. Combining Proofs and Programs.

Coffee Break (10:00-10:30)

Session 10 (10:30-12:10)

Chair: Aleksy Schubert

10:30-11:00 Takahito Aoto, Toshiyuki Yamada, and Yuki Chiba. Natural Inductive Theorems for Higher-Order Rewriting.

11:00-11:30 Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise. Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.

11:30-12:00 Jonathan Kochems and Luke Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars.

12:00-12:15 René Thiemann Results of the 2011 Termination Competition (termComp 2011).

Lunch Break (12:10-14:00)

Session 11 (14:00-15:30)

Chair: Aart Middeldorp

14:00-14:30 Martin Avanzini, Naohi Eguchi, and Georg Moser. A Path Order for Rewrite Systems that Compute Exponential Time Functions.

14:30-15:00 Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity.

15:00-15:30 Takahito Aoto and Yoshihito Toyama. A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems.

Coffee Break (RTA + TLCA Meeting) (15:30-16:30)

Excursion and Conference Dinner (16:30-00:00)

16:30-20:30 Excursion.

20:30-00:00 Conference Dinner.

Wednesday, June 1st

Session 1 (09:00-10:00)

Chair: Luke Ong

09:00-10:00 Invited talk: Stephanie Weirich. Combining Proofs and Programs.

10:00-10:15 TLCA Opening and Welcome

Coffee Break (10:15-10:30)

Session 2 (10:30-12:00)

Chair: Hugo Herbelin

10:30-11:00 Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for PiSigma.

11:00-11:30 Aloïs Brunel, Clément Houtmann and Olivier Hermant. Orthogonality and boolean algebras for deduction modulo.

11:30-12:00 Zena M Ariola, Hugo Herbelin and Alexis Saurin. Classical call-by-need and duality.

Lunch Break (12:00-14:00)

Session 3 (14:00-15:30)

Chair: Mariangiola Dezani-Ciancaglini

14:00-14:30 Pierre Bourreau and Sylvain Salvati. Game semantics and uniqueness of type inhabitance in the simply-typed lambda-calculus.

14:30-15:00 Steffen Van Bakel, Franco Barbanera and Ugo De Liguoro. A Filter Model for lambda-mu.

15:00-15:30 Steffen Van Bakel and Reuben Rowe. Approximation semantics and expressive predicate assignment for object-oriented programming.

Coffee Break (RTA + TLCA Meeting) (15:30-16:30)

Excursion and Conference Dinner (16:30-00:00)

16:30-20:30 Excursion.

20:30-00:00 Conference Dinner.

Thursday, June 2nd

Session 4 (09:00-10:00)

Chair: Thorsten Altenkirch

09:00-10:00 Invited talk: Vladimir Voevodsky. TBA.

Coffee Break (10:00-10:30)

Session 5 (10:30-12:00)

Chair: Ralph Matthes

10:30-11:00 Peter Arndt and Krzysztof Kapulkin. Homotopy theoretic models of type theory.

11:00-11:30 Pierre Clairambault and Peter Dybjer. The biequivalence of locally cartesian closed categories and Martin-Löf type theories.

11:30-12:00 Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski. Partiality, state and dependent types.

Lunch Break (12:00-14:00)

Session 6 (14:00-15:30)

Chair: Luke Ong

14:00-14:30 Marc Lasson. Controlling program extraction in light logics.

14:30-15:00 Antoine Madet and Roberto M. Amadio. An elementary affine lambda calculus with multithreading and side effects.

15:00-15:30 Giulio Manzonetto and Michele Pagani. Bohm theorem for resource lambda calculus through Taylor expansion.

Coffee Break (15:30-16:00)

TLCA Business Meeting (16:00-17:00)

Friday, June 3rd

Session 7 (09:00-10:00)

Chair: Silvia Ghilezan

09:00-10:00 Invited talk: Alexandre Miquel. A survey of classical realizability.

Coffee Break (10:00-10:30)

Session 8 (10:30-12:00)

Chair: Roger Hindley

10:30-11:00 Stéphane Gimenez. Realizability proof for normalization of full differential linear logic.

11:00-11:30 Jakob Rehof and Pawel Urzyczyn. Finite combinatory logic with intersection types.

11:30-12:00 Luca Roversi. Linear lambda calculus and deep inference.

Lunch and Closing (12:00-14:00)