HOR on Wednesday, July 14th

09:00‑10:00 Session 1
Location: IF G.07
09:00 Maribel Fernández (Invited Speaker)
Closed nominal rewriting: properties and applications
10:30‑12:30 Session 2
Location: IF G.07
10:30 Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson and Benoît Valiron
Equivalence of algebraic λ-calculi

We examine the relationship between the algebraic λ-calculus (λalg) [Vau09] a fragment of the differential λ-calculus [ER03]; and the linear-algebraic λ-calculus (λlin) [AD08], a candidate λ-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and the set of terms is closed under linear combinations. We answer the conjectured question of the simulation of λalg by λlin [AV09] and the reverse simulation of λlin by λalg. Our proof relies on the observation that λlin is essentially call-by-value, while λalg is call-by-name. The former simulation uses the standard notion of thunks, while the latter is based on an algebraic extension of the continuation passing style. This result is a step towards an extension of call-by-value / call-by-name duality to algebraic λ-calculi.

11:00 Harald Zankl, Nao Hirokawa and Aart Middeldorp
Uncurrying for Innermost Termination and Derivational Complexity

In this paper we investigate the uncurrying transformation from (Hirokawa et al., 2008) for innermost termination and derivational complexity.

11:30 Giulio Manzonetto and Paolo Tranquilli
A Calculus of Coercions Proving the Strong Normalization of MLF

We provide a strong normalization result for MLF, a type system generalizing ML with first-class polymorphism as in system F. The proof is achieved by translating MLF into a calculus of coercions, and showing that this calculus is just a decorated version of system F. Simulation results then entail strong normalization from the same property of system F.

12:00 Cynthia Kop (student talk)
A new formalism for higher-order rewriting
14:00‑15:00 Session 3
Location: IF G.07
14:00 Silvia Ghilezan (Invited Speaker)
Computational interpretations of logic
15:30‑17:30 Session 4
Chair: Mariangiola Dezani-Ciancaglini
Location: IF G.07
15:30 Thibaut Balabonski
On the Implementation of Dynamic Patterns

Pattern matching against dynamic patterns in functional programming languages is modelled in the Pure Pattern Calculus by one single meta-rule. The present contribution is a refinement which narrows the gap between the abstract calculus and the implementation, and allows the reasoning on matching algorithms and strategies.

16:00 Kristoffer Rose
Higher-order Rewriting for Executable Compiler Specifications

In this paper I show how a simple compiler can be completely specified using higher order rewriting in all stages of the compiler: parser, analysis/optimization, and code generation, specifically using the crsx.sf.net system for a small declarative language called ``X'' inspired by XQuery (for which I am building a production compiler in the same way).

16:30 Ariel Mendelzon, Alejandro Ríos and Beta Ziliani
Swapping: a natural bridge between named and indexed explicit substitution calculi

This article is devoted to the presentation of lambda-rex, an explicit substitution calculus with de Bruijn indexes and an elegant notation. By being isomorphic to lambda-ex –- a state-of-the-art formalism with variable names –-, lambda-rex accomplishes simulation of beta-reduction (Sim), preservation of beta-strong normalization (PSN) and metaconfluence (MC), among other desirable properties. Our calculus is based on a novel presentation of lambda-dB, using a peculiar swap notion that was originally devised by de Bruijn. Besides lambda-rex, two other indexed calculi isomorphic to lambda-x and lambda-xgc are presented, demonstrating the potential of our technique when applied to the design of indexed versions of known named calculi.

17:00 Delia Kesner, Carlos Lombardi and Alejandro Ríos
Standardisation for constructor based pattern calculi

This work gives some insights and results on standardisation for call by name pattern calculi. More precisely, we define standard reductions for a pattern calculus with constructor-based data terms and patterns. This notion is based on reduction steps that are needed to match an argument with respect to a given pattern.

We prove the standardisation theorem by using the technique developed by Takahashi and Crary for lambda-calculus. The proof is based on the fact that any development can be specified as a sequence of head steps followed by internal reductions, i.e. reductions in which no head steps are involved.

We expect to extend these results to more complex calculi with open and dynamic patterns.