The
First workshop on the rho-calculus
took place at
LORIA (Nancy,France)
the 11 and 12 March, 2004. The aims of this workshop were
twofold. First, to present the rho-calculus focusing on recent works
and second, to understand how these works relate to other ones. The
program and the slides of the talks are available below. The
discussed topics included:
- Combination of lambda-calculus and rewriting (including a general
presentation of the rho-calculus and a talk on termination).
- Types and rho-calculus (including a presentation
of the Pure Pattern Type Systems and of normalization problems).
- Implementation issues (including a presentation
of the imperative rho-calculus, a presentation of Rogue, a
presentation of the rho-calculus with explicit constraint handling).
- Higher-order unification/matching in the rho-calculus
- Applications of rho-calculus (including a talk on
+rho-calculus and quantum calculus)
Program:
Thursday 11 mars
- Session 1
- 09:00--10:30 Discussion session
- 10:30--11:00 Break
- 11:00--12:00 The plain untyped Rho-Calculus (syntax,
matching, semantics, examples, expressivity): Claude, Horatiu
Download The slides.
- 12:00--12:30 Nominal rewriting: Maribel
Download The slides.
- 12:30--13:00 Extensions of Nominal Rewriting: Murdoch
Download The slides.
- 13:00--14:30 Lunch
- Session 2
- 14:30--15:30 Validating Constructive Metatheory with Rogue-Sigma-Pi:
Aaron
Download The slides.
- 15:30--16:00 Type systems for the Rho-Calculus (simple and
polymorphic types): Benjamin
Download The slides.
- 16:00--16:30 Break
- 16:30--17:15 Pure Pattern Type Systems: Luigi
Download The slides.
- 17:30--18:30 Strong Normalization in the Rho-Cube - the first-order type system: Benjamin
Download The slides.
Friday 12 mars
- Session 3
- 09:00--9:30 Combining lambda-calculus and rewriting: brief history and open problems: Frederic
Download The slides.
- 9:30--10:00 Rewriting and Quantum Calculus: Pablo
Download The slides.
- 10:00--10:30 Break
- 10:30--11:00 Imperative Rho-Calculus: Luigi
Download The slides.
- 11:00--12:30 Implementing the Rho-Calculus: talk by Germain (A Rho-Calculus of explicit constraint application) and discussion session (inc. TOM)
Download The slides.
- 12:30--14:00 Lunch
- Session 4
- 14:00--14:30 Rho-Calculus and Quantum Calculus: Gilles
Download The slides.
- 14:30--15:00 A Rho-Calulus for graph rewriting: Clara
Download The slides.
- 15:00--16:30 Discussion and dream session (Lazy rho-calculus, second-order matching in the Rho-Calculus)
Some pictures taken during talks
Pict.1 Pict.2 Pict.3 Pict.4
List of participants:
- Pablo Arrighi
- Clara Bertolissi
- Frederic Blanqui
- Horatiu Cirstea
- Eric Deplagne
- Gilles Dowek
- Germain Faure
- Maribel Fernandez
- Julien Forest
- Murdoch Gabbay
- Therese Hardin
- Dan Hernest
- Sebastien Hinderer
- Mathieu Jaume
- Jean-Pierre Jouannaud
- Claude Kirchner
- Luigi Liquori
- Fabrice Nahon
- Virgile Prevosto
- Francois-Regis Sinot
- Aaron Stump
- Benjamin Wack