About Conferences Colloquium Workshops Practical

HOR 2007 Programme

Monday, June 25, 2007



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.

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.

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.

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).


webmaster at rdp07 dot org