About Conferences Colloquium Workshops Practical

RDP'07 Complete Programme Day by Day

Print Version (postscript) - printouts will also be distributed at the conference.


Monday, June 25


8:15 - 9:00      Arrival of participants and registration

       HOR Session 1 (Room 35-2-25)
9:00 - 10:00      Carsten Schürmann. On the formalization of logical relation arguments in Twelf. (Invited talk)
10:00 - 10:30      Kristoffer Rose. CRSX - an open source platform for experiments with higher-order rewriting.

       PATE Sesssion 1 (Room 35-3-35)
9:00 - 10:00      Bill Farmer. The Use of Formal Reasoning Technology in Mathematics Education: Opportunities and Challenges. (Invited talk)
10:00 - 10:30      Claudio Sacerdoti Coen and Enrico Zoli. A Note on Formalising Undefined Terms in Real Analysis.

       WFLP Session 1: FLP Languages (Room 35-3-26)
8:50 - 9:00      Welcome.
9:00 - 9:30      Sebastian Fischer, Josep Silva, Salvador Tamarit and German Vidal. Towards a Safe Partial Evaluation of Lazy Functional Logic Programs.
9:30 - 10:00      Bernd Brassel, Sebastian Fischer and Frank Huch. Declaring Numbers.
10:00 - 10:30      Emilio Jesús Gallego Arias, Julio Mariño and Jose Maria Rey. A Generic Semantics for Constraint Functional Logic Programming.

       WRS Session 1 (Room 35-3-28)
8:50 - 9:15      René Thiemann, Aart Middeldorp. Innermost Termination of Rewrite Systems by Labeling.
9:15 - 9:40      Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe. Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems.
9:40 - 10:05      Felix Schernhammer, Bernhard Gramlich. Termination of Lazy Rewriting Revisited.
10:05 - 10:30      Masahiko Sakai, Yi Wang. Undecidable Properties on Length-Two String Rewriting Systems.

10:30 - 11:00      Coffee Break

       HOR Session 2 (Room 35-2-25)
11:00 - 11:30      Daniel Ventura, Mauricio Ayala-Rincón and Fairouz Kamareddine. Principal typings for explicit substitutions calculi.
11:30 - 12:00      Takahito Aoto and Toshiyuki Yamada. Argument filterings and usable rules for simply typed dependency pairs.
12:00 - 12:30      Andreas Abel. Syntactical strong normalization for intersection types with term rewriting rules.

       PATE Session 2 (Room 35-3-35)
11:00 - 11:30      Agnieszka Kozubek and Pawel Urzyczyn. In the search of a naive type theory.
11:30 - 12:00      Adam Naumowicz. How to Teach to Write a Proof.
12:00 - 12:30      Serge Autexier and Marc Wagner. Status Report on the Tight Integration of a Scientific Text-Editor and a Proof Assistance System.

       WFLP Session 2: Theory (Room 35-3-26)
11:00 - 11:30      Murdoch Gabbay and Michael Gabbay. a-logic with an arrow.
11:30 - 12:00      Javier Álvez and Paqui Lucio. A Decision Procedure for Non-failure in CLP.
12:00 - 12:30      Wolfram Kahl. Lazy Call-By-Value in the Pattern Matching Calculus - Towards Equational Reasoning for Functional-Logic Programming.

       WRS Session 2 (Room 35-3-28)
11:00 - 11:40      Pierre-Etienne Moreau, Antoine Reilles. Rules and Strategies in Java. (Invited Talk)
11:40 - 12:05      Dorel Lucanu, Grigore Rosu, Gheorghe Grigoras. Regular Strategies as Proof Tactics for CIRC.
12:05 - 12:30      Malgorzata Biernacka, Dariusz Biernacki. Formalizing Constructions of Abstract Machines for Functional Languages in Coq.

12:30 - 14:00      Lunch

       HOR Session 3 (Room 35-2-25)
14:00 - 15:00      Tarmo Uustalu. Circular proofs = Mendler in sequent form. (Invited Talk)
15:00 - 15:30      Lionel Marie-Magdeleine and Serguei Soloviev. Non-standard reductions in simply-typed, higher order and dependently-typed systems.

       PATE Session 3 (Room 35-3-35)
14:00 - 14:30      Jérémy Blanc, André Hirschowitz, Loïc Pottier. Proofs for freshmen with Coqweb.
14:30 - 15:00      Cezary Kaliszyk, Freek Wiedijk, Maxim Hendriks, Femke van Raamsdonk. Teaching logic using a state-of-the-art proof assistant.
15:00 - 15:30      Jakub Sakowicz and Jacek Chrzaszcz. Papuq: a Coq assistant.

       WFLP Session 3: Debugging and tests (Room 35-3-26)
14:00 - 14:30      Wolfgang Lux. Declarative Debugging Meets the World.
14:30 - 15:00      Rafael Caballero-Roldan, Yolanda García-Ruiz and Fernando Sáenz-Pérez. A New Proposal for Debugging Datalog Programs.
15:00 - 15:30      Ron van Kesteren, Olha Shkaravska and Marko van Eekelen. Inferring static non-monotonically sized types through testing.

       WRS Session 3 (Room 35-3-28)
14:00 - 14:40      Rachid Echahed. On Term-Graph Rewrite Strategies. (Invited Talk)
14:40 - 15:05      Paolo Baldan, Clara Bertolissi, Horatiu Cirstea,Claude Kirchner. Towards a sharing strategy for the graph rewriting calculus.
15:05 - 15:30      Francois-Régis Sinot. Complete Laziness.

15:30 - 16:00      Coffee Break

       HOR Session 4 (Room 35-2-25)
16:00 - 16:30      Lisa Allali. Algorithmic equality in Heyting arithmetic modulo.
16:30 - 17:00      Max Schäfer. Elements of a categorical semantics for the Open Calculus of Constructions.
17:00 - 17:30      Kristoffer Rose. Demonstration of CRSX (System demo).

       PATE Session 4 (Room 35-3-35)
16:00 - 17:00      René David and Christophe Raffalli. Some considerations about proof assistants for education.

       WFLP Session 4: Applications (Room 35-3-26)
16:00 - 16:30      Tetsuo Ida, Mircea Marin and Hidekazu Takahashi. Computational Origami Construction as Constraint Solving and Rewriting.
16:30 - 17:00      Michele Baggi and Demis Ballis. PHIL: A Lazy Implementation of a Language for Approximate Filtering of XML Documents.
17:00 - 17:30      Alexei Lescaylle and Alicia Villanueva. Using tccp for the Specification and Verification of Communication Protocols.

       WRS Session 4 (Room 35-3-28)
16:00 - 16:25      Victor Winter. Stack-based Strategic Control.
16:25 - 16:50      Elena Machkasova. Computational Soundness of a Call by Name Calculus of Recursively-scoped Records.
16:50 - 17:15      Sandra Alves, Mário Florido, Ian Mackie, Francois-Régis Sinot. Minimality in a Linear Calculus with Iteration.
17:15 - 17:40      José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaca. Token-passing Nets for Functional Languages.

Tuesday, June 26


8:15 - 9:00      Arrival of participants and registration

       RTA/TLCA joint invited speaker (Amphithéâtre Jean Fourastié)
    Chair: Femke van Raamsdonk
8:55 - 9:00      Welcome.
9:00 - 10.00      Frank Pfenning. On a Logical Foundation for Explicit Substitutions.

10.00 - 10.30      Coffee Break

       RTA Session 2: regular papers (Amphithéâtre Jean Fourastié)
    Chair: Delia Kesner
10:30 - 11:00      Kentaro Kikuchi. Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi.
11:00 - 11:30      José Espírito Santo. Delayed Substitutions.
11:30 - 12:00      Horatiu Cirstea and Germain Faure. Confluence of Pattern-Based Calculi.
12:00 - 12:30      Lionel Vaux. On Linear Combinations of λ-Terms.

       TLCA Session 2 (Amphithéâtre Jean Prouvé)
    Chair: Paula Severi
10:30 - 11:00      Marcelo Fiore. Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic.
11:00 - 11:30      Ying Jiang and Guo-Qiang Zhang. Weakly Distributive Domains.
11:30 - 12:00      Neil Ghani and Patricia Johann. Initial Algebra Semantics is Enough!
12:00 - 12:30      William Blum and Luke Ong. The Safe Lambda Calculus.

12:30 - 14:00      Lunch

       RTA Session 3: system descriptions (Amphithéâtre Jean Fourastié)
    Chair: Salvador Lucas
14:00 - 14:20      Emilie Balland, Paul Brauner, Radu Kopetz, Pierre-Etienne Moreau, Antoine Reilles. Tom: Piggybacking Rewriting on Java.
14:20 - 14:40      Mark Hills, Grigore Rou. KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis.
14:40 - 15:00      Claude Marché, Johannes Waldmann, Hans Zantema. The Termination Competition 2007.

       TLCA Session 3 (Amphithéâtre Jean Prouvé)
    Chair: Pawel Urzyczyn
14:00 - 14:30      Benedetto Intrigila and Richard Statman. The Omega Rule is Π11 Complete in the Lambda-Calculus.
14:30 - 15:00      Sam Lindley. Extensional rewriting with sums.

15:00 - 15:30      Coffee Break

       RTA Session 4: regular papers (Amphithéâtre Jean Fourastié)
    Chair: Jürgen Giesl
15:30 - 16:00      Martin Korp and Aart Middeldorp. Proving Termination of Rewrite Systems using Bounds.
16:00 - 16:30      Hans Zantema and Johannes Waldmann. Termination by Quasi-Periodic Interpretations.
16:30 - 17:00      Harald Zankl and Aart Middeldorp. Satisfying KBO Constraints.
17:00 - 17:30      Temur Kutsia, Jordi Levy and Mateu Villaret. Sequence Unification Through Currying.

       TLCA Session 4 (Amphithéâtre Jean Prouvé)
    Chair: Simone Martini
15:30 - 16:00      Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction.
16:00 - 16:30      Jose Espirito Santo. Completing Herbelin's Programme.
16:30 - 17:00      Jose Espirito Santo, Ralph Matthes and Luís Pinto. Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi.

       TLCA business meeting (Amphithéâtre Jean Prouvé)
17:10 - 18:00      TLCA business meeting.

       RDP Reception (Chapel)
18:00 - 22:00      Reception, with an evening talk by Henk Barendregt. The Diamond Anniversary of Lambda Calculus.

Wednesday, June 27


8:15 - 9:00      Arrival of participants

       RTA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Manfred Schmidt-Schauß
9:00 - 10.00      Xavier Leroy. Formal Verification of an Optimizing Compiler.

10:00 - 10:30      Coffee Break

       RTA Session 6: regular papers (Amphithéâtre Jean Fourastié)
    Chair: Ralf Treinen
10:30 - 11:00      Yohan Boichut, Thomas Genet, Thomas Jensen and Luka Le Roux. Rewriting Approximations for Fast Prototyping of Static Analyzers.
11:00 - 11:30      Santiago Escobar and José Meseguer. Symbolic Model Checking of Infinite-State Systems Using Narrowing.
11:30 - 12:00      Siva Anantharaman, Paliath Narendran and Michael Rusinowitch. Intruders with Caps.
12:00 - 12:30      Irène Anne Durand and Géraud Sénizergues. Bottom-Up Rewriting is Inverse Recognizability Preserving.

       TLCA Session 6 (Amphithéâtre Jean Prouvé)
    Chair: Healf Goguen
10:30 - 11:00      Makoto Tatsuta. Simple saturated sets for disjunction and second-order existential quantification.
11:00 - 11:30      René David and Karim Nour. An arithmetical proof of the strong normalization for the lambda-calculus with recursive equations on types.
11:30 - 12:00      Andreas Abel. Strong Normalization and Equi-(co)inductive Types.
12:00 - 12:30      Dariusz Kusmierek. The inhabitation problem for rank two intersection types.

12:30 - 14:00      Lunch

       TLCA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Frank Pfenning
14:00 - 15:00      Greg Morrisett. The Marriage of Dependent Types and Effects.

15:00 - 15:30      Coffee Break

       RTA Session 8: regular papers (Amphithéâtre Jean Fourastié)
    Chair: Hélène Kirchner
15:30 - 16:00      Manfred Schmidt-Schauß. Correctness of Copy in Calculi with Letrec.
16:00 - 16:30      Joe Hendrix and José Meseguer. On the Completeness of Context-Sensitive Order-Sorted Specifications.
16:30 - 17:00      Rachid Echahed and Nicolas Peltier. Non Strict Confluent Rewrite Systems for Data-Structures with Pointers.
17:00 - 17:30      Dominique Duval, Rachid Echahed and Frederic Prost. Adjunction for Garbage Collection with Application to Graph Rewriting.

       TLCA Session 8 (Amphithéâtre Jean Prouvé)
    Chair: Peter Dybjer
15:30 - 16:00      Sylvain Boulmé. Intuitionistic Refinement Calculus.
16:00 - 16:30      Oleg Kiselyov and Chung-chieh Shan. A Substructural Type System for Delimited Continuations.
16:30 - 17:00      Ana Bove and Venanzio Capretta. Computation by Prophecy.
17:00 - 17:30      Denis Cousineau and Gilles Dowek. Embedding Pure Type Systems in the lambda Pi calculus modulo.

       RDP/RTA business meetings (Amphithéâtre Friedmann)
17:45 - 18:15      RDP business meeting.
18:15 - 19:15      RTA business meeting.

21:00 - 23:00      RDP Banquet

Thursday, June 28


8:15 - 9:00      Arrival of participants

       TLCA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Simona Ronchi Della Rocca
9:00 - 10.00      Patrick Baillot. From Proof-Nets to linear Logic Type Systems for Polynomial Time Computing.

10:00 - 10:30      Coffee Break

       RTA Session 10: regular papers (Amphithéâtre Jean Fourastié)
    Chair: Roberto di Cosmo
10:30 - 11:00      Makoto Tatsuta. The Maximum Length of Mu-Reduction in Lambda Mu-Calculus.
11:00 - 11:30      Gilles Dowek and Olivier Hermant. A Simple Proof that Super-Consistency Implies Cut Elimination.
11:30 - 12:00      Lutz Straßburger. A Characterisation of Medial as Rewriting Rule.
12:00 - 12:30      Thierry Boy de la Tour and Mnacho Echenim. Determining Unify-Stable Presentations.

       TLCA Session 10 (Amphithéâtre Jean Prouvé)
    Chair: Patrick Baillot
10:30 - 11:00      Jean-Yves Marion. Predicative analysis of feasibility and diagonalisation.
11:00 - 11:30      Olha Shkaravska, Ron van Kesteren and Marko van Eekelen. Polynomial Size Analysis of First-Order Functions.
11:30 - 12:00      Stefano Berardi. An Semantic for Intuitionistic Arithmetic based on Tarski Games.
12:00 - 12:30      James Lipton and Susana Nieva. Higher Order Logic Programming Languages with Constraints: a Semantics.

12:30 - 14:00      Lunch

       RTA invited talk (Amphithéâtre Jean Fourastié)
    Chair: Franz Baader
14:00 - 15:00      Robert Nieuwenhuis. Challenges in Satisfiability Modulo Theories.

       Longo Symposium Session 1: Lessons from Logic and Physics (Amphithéâtre 3)
13:30 - 14:00      Arrival of participants and registration.
14:00 - 14:10      Welcome.
14:10 - 14:50      Mioara Mugur-Schächter. On the patient quest of Giuseppe Longo for a general unity and coherence.
14:50 - 15:30      Jean-Yves Girard. Truth, modality, intersubjectivity.

15:00 - 15:30      RTA/TLCA Coffee Break
15:30 - 16:00      Longo Symposium Coffee Break

       RTA Session 12: regular papers (Amphithéâtre Jean Fourastié)
    Chair: Sophie Tison
15:30 - 16:00      Vincent van Oostrom. Random Descent.
16:00 - 16:30      Guillem Godoy, Eduard Huntingford and Ashish Tiwari. Termination of Rewriting with Right-Flat Rules.
16:30 - 17:00      Rémy Haemmerlé and François Fages. Abstract Critical Pairs and Confluence of Arbitrary Binary Relations.
17:00 - 17:30      Guillem Godoy and Eduard Huntingford. Innermost-Reachability and Innermost-Joinability are Decidable for Shallow Term Rewrite Systems.

       TLCA Session 12 (Amphithéâtre Jean Prouvé)
    Chair: Olivier Laurent
15:30 - 16:00      Damiano Mazza. Edifices: Boehm Trees for the Interaction Combinators.
16:00 - 16:30      Claudia Faggian and Mauro Piccolo. Ludics is a model for the (finitary) linear Pi-calculus.
16:30 - 17:00      Dimitris Mostrous and Nobuko Yoshida. Two Session Typing Systems for Higher-Order Mobile Processes.
17:00 - 17:30      Lionel Vaux. Convolution lambda-bar-mu-calculus.

       Longo Symposium Session 2: Geometry and Cognition (Amphithéâtre 3)
16:00 - 16:40      Jean Petitot. Neurogeometry and the origin of space.

       Longo Symposium Session 3: Models and Categories (Amphithéâtre 3)
16:40 - 17:20      Eugenio Moggi. Category Theory and Lambda Calculus.
17:20 - 18:00      Martin Hyland. Modelling the Impossible.

Friday, June 29


8:15 - 9:00      Arrival of participants and registration

       Longo Symposium Session 4: Lambda Calculus (Amphithéâtre A)
9:00 - 9:40      Henk Barendregt and Jan Willem Klop. Non-left linear reductions via infinitary lambda calculus.
9:40 - 10:20      Furio Honsell and Gordon Plotkin. On the βη-completeness and expressiveness of some classes of combinatory algebras.

       RULE Session 1 (Room 35-3-28)
9:15 - 10:00      Tim Furche. Web Rules!
10:00 - 10:30      Gurvan Le Guernic and Julien Perret. FLIC: Application to Caching of a Dynamic Dependency Analysis for a 3D Oriented CRS.

       SecReT/UNIF joint invited talk (Room 35-3-26)
9:30 - 10:30      Thomas Genet. Rewriting and Reachability for Software Security.

       WST Session 1: Matrices and Dependency Pairs (Room 35-2-25)
9:00 - 9:15      Johannes Waldmann. Arctic Termination.
9:15 - 9:30      Andreas Gebhardt, Dieter Hofbauer and Johannes Waldmann. Matrix Evolutions.
9:30 - 9:45      Adam Koprowski and Hans Zantema. Certification of Matrix Interpretations in Coq.
9:45 - 10:00      Jürgen Giesl, René Thiemann, Stephan Swiderski and Peter Schneider-Kamp. Termination of TRSs with Bounded Increase.
10:00 - 10:15      Jörg Endrullis and Jeroen Ketema. Root Stabilisation Using Dependency Pairs.
10:15 - 10:30      Beatriz Alarcón, Raúl Gutiérrez and Salvador Lucas. Improving Termination Proofs of Context-Sensitive Rewriting using Dependency Pairs.

10:30 - 11:00      Workshop Coffee Break
10:20 - 10:40      Longo Symposium Coffee Break

       Longo Symp. 5: Theoretical Biology and Biological Theories (Amphithéâtre A)
10:40 - 11:20      Pierre-Louis Curien. Computational self-assembly.
11:20 - 12:00      Luca Cardelli. Artificial Biochemistry.
12:00 - 12:40      John Stewart. Is “life” computable?.

       RULE Session 2 (Room 35-3-28)
11:00 - 11:30      Juan Antonio Guerrero and Ginés Moreno. Fuzzy Folding/Unfolding and Related Transformation Rules.
11:30 - 12:00      Malte Appeltauer and Günter Kniesel. Towards Generic Pointcut-Driven Program Transformation Rules.
12:00 - 12:30      Emilie Balland, Pierre-Etienne Moreau and Antoine Reilles. Optimising Strategies in a Rule Based Framework.

       SecReT Session 2 (Room 35-3-26)
11:00 - 11:30      Steve Barker and Maribel Fernández. Action-Status Access Control as Term Rewriting.
11:30 - 12:00      Charles Morisset and Anderson Santana de Oliveira. Automated Detection of Information Leakage in Access Control.
12:00 - 12:30      Charles Morisset and Anderson Santana de Oliveira. Demo Tom.

       UNIF Session 2 (Room 35-3-35)
11:00 - 11:30      Benjamin Carle, Paliath Narendran and Colin Sheriff. On extended regular expressions.
11:30 - 12:00      Sylvain Conchon, Évelyne Contejean and Johannes Kanig. Combining Equality and Solvable Theories.
12:00 - 12:30      Sylvain Conchon, Évelyne Contejean and Johannes Kanig. Demo Ergo.

       WST Session 2: Programming languages (Room 35-2-25)
11:00 - 11:15      Dean Voets, Paolo Pilozzi and Danny De Schreye. A new approach to termination analysis of Constraint Handling Rules.
11:15 - 11:30      Paolo Pilozzi, Tom Schrijvers and Danny De Schreye. Proving termination of CHR in Prolog: A transformational approach.
11:30 - 11:45      Amir Ben-Amram and Chin Soon Lee. Ranking Functions for Size-Change Termination II.
11:45 - 12:00      Elvira Albert, Puri Arenas, Michael Codish, Samir Genaim, German Puebla and Damiano Zanardini. Termination Analysis of Java Bytecode.
12:00 - 12:15      Keiko Nakata and Jacques Garrigue. Path resolution for recursive nested modules is undecidable.
12:15 - 12:30      Nikolaj Popov and Tudor Jebelean. Proving Termination of Recursive Programs by Matching Against Simplified Program Versions and Construction of Specialized Libraries in Theorema.

12:30 - 14:00      Workshop Lunch
12:40 - 14:00      Longo Symposium Lunch

       Longo Symposium Session 6: Types for Object-Orientation (Amphithéâtre A)
14:00 - 14:40      Mariangiola Dezani. Session Types for Object-Oriented Languages.
14:40 - 15:20      Kim Bruce. Modularity and Scope in Object-Oriented Languages.

       RULE Session 3 (Room 35-3-28)
14:00 - 14:30      Delia Kesner. Parametric resources for lambda-calculi. Invited talk.
14:30 - 15:00      Ozan Kahramanogullari. Maude as a Platform for Designing and Implementing Deep Inference Systems.
15:00 - 15:30      Oana Andrei and Hélène Kirchner. Towards a Rewriting Calculus for Multigraphs with Ports.

       SecReT Session 3 (Room 35-3-26)
14:00 - 14:30      Santiago Escobar, Joe Hendrix, Catherine Meadows, and José Meseguer. Diffie-Hellman Cryptographic Reasoning in the Maude-NRL Protocol Analyzer.
14:30 - 15:00      Santiago Escobar, Joe Hendrix, Catherine Meadows, and José Meseguer. Demo Maude-NPA.
15:00 - 15:30      Anders Moen Hagalisletto and Olaf Owe. Local Deduction of Trust.

       UNIF Session 3 (Room 35-3-35)
14:00 - 14:30      Viorica Sofronie-Stokkermans. On unification in certain finitely generated varieties of algebras.
14:30 - 15:00      Ginés Moreno and Vicente Pascual. Similarity-based Unification Embedded into Narrowing.
15:00 - 15:30      Martin Plümicke. Java type unification with wildcards.

       WST Session 3: Satisfiability and Constraint Solving (Room 35-2-25)
14:00 - 14:15      Harald Zankl and Aart Middeldorp. Nontermination of String Rewriting using SAT.
14:15 - 14:30      Peter Schneider-Kamp, René Thiemann, Elena Annov, Michael Codish and Jürgen Giesl. Implementing RPO using SAT.
14:30 - 14:45      Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann and Harald Zankl. SAT Solving for Termination Analysis with Polynomial Interpretations.
14:45 - 15:00      Salvador Lucas. Solving polynomial constraints over the reals in proofs of termination.
15:00 - 15:15      Salvador Lucas and Rafael Navarro. Fast SAT-based polynomial constraint solving for termination tools.
15:15 - 15:30      Claude Marché, Johannes Waldmann, Hans Zantema. The Termination Competition 2007.

15:30 - 16:00      Workshop Coffee Break
15:20 - 15:40      Longo Symposium Coffee Break

       Longo Symp. 7: Analysis, Physics, and Recursion Theory (Amphithéâtre A)
15:40 - 16:20      Abbas Edalat. Recursively measurable sets and computable measurable sets.
16:20 - 17:00      Thierry Paul. Semiclassical analysis and sensitivity to initial data.

       Longo Symposium Closing Session (Amphithéâtre A)
17:00 - 17:50      Giuseppe Longo. From exact sciences to life phenomena: a few concluding remarks on Bohr and Schrödinger.

       RULE Session 4 (Room 35-3-28)
16:00 - 16:30      Demis Ballis, Andrea Baruzzo and Marco Comini. A Rule-based Method to Match Software Patterns against UML Models.
16:30 - 17:00      José Bacelar Almeida, Jorge Sousa Pinto and Miguel Vilaça. A Tool for Programming with Interaction Nets.
17:00 - 17:30      Discussion.

       SecReT Session 4 (Room 35-3-26)
16:00 - 16:30      Anders Moen Hagalisletto and Olaf Owe. Demo Maude-PROSA.
16:30 - 17:00      Discussion and Business Meeting.

       UNIF Session 4 (Room 35-3-35)
16:00 - 16:30      Claude Kirchner, Radu Kopetz and Pierre-Etienne Moreau. Anti-Pattern Matching Modulo.
16:30 - 17:00      Discussion and Business Meeting.

       WST Session 4: Conditional Rewriting and Proof Calculi (Room 35-2-25)
16:00 - 16:15      Naoki Nishida, Masahiko Sakai and Terutoshi Kato. Convergent Term Rewriting Systems for Inverse Computation of Injective Functions.
16:15 - 16:30      Felix Schernhammer and Bernhard Gramlich. On Proving and Characterizing Operational Termination of Deterministic Conditional Rewrite Systems.
16:30 - 16:45      Daniel Dougherty, Silvia Ghilezan and Pierre Lescanne. A General Technique for Analyzing Termination in Symmetric Proof Calculi.
16:45 - 17:00      James Brotherston, Richard Bornat and Cristiano Calcagno. A Cyclic Termination Proof of In-Place List Reversal using Separation Logic.
17:00 - 17:30      WST business meeting.

webmaster at rdp07 dot org