HOR on Tuesday, August 15th

Invited Talk (09:00‑10:00)

09:00‑10:00

Eelco Visser (University of Utrecht) Dynamic rewrite rules [pdf] The Stratego program transformation language is based on term rewriting, but extends the formalism with programmmable rewriting strategies and scoped dynamic rewrite rules. In the talk I will give an introduction to dynamic rewrite rules in Stratego illustrated by means of examples from program transformation.

Break (10:00‑10:30)

Session 1 (10:30‑12:00)

10:30‑11:00	Thomas Ehrhard and Olivier Laurent Embedding the finitary Pi-calculus in differential interaction nets
11:00‑11:30	Caroline Priou Non-deterministic Bohm trees
11:30‑12:00	Barry Jay Typing the pattern calculus

Lunch break (12:30‑14:00)

Session 2 (14:00‑15:30)

14:00‑14:30	Barry Jay Quantifying the benefits of sub-typing
14:30‑15:00	Nao Hirokawa and Aart Middeldorp Uncurrying for termination
15:00‑15:30	Shane O'Conchuir Proving PSN by simulating non-cal substitution with local substitution

Break (15:30‑16:00)

Invited Talk (16:00‑17:00)

16:00‑17:00

Hugo Herbelin (INRIA Futurs) The duality of computation [pdf] The work presented here is an extension of a previous work realised jointly with Pierre-Louis Curien. The current work focuses on the pure calculus of variables and binders that operates at the core of the duality between call-by-name and call-by-value evaluations. A Curry-Howard-de Bruijn correspondence is given that shed light on some aspects of Gentzen's sequent calculus. This includes a sequent-free presentation of it.