La première rencontre de l'édition 2011 du projet se tiendra le lundi 18
juillet 2011 à l'IML
à Marseille.
Exposés
- 09h40-10h00: Accueil.
- 10h00-11h00 Alejandro Díaz-Caro (joint work with Pablo
Buiras and Mauro Jaskelioff):
Confluence via strong normalisation in an algebraic λ-calculus with rewriting.
- The linear-algebraic λ-calculus and the algebraic λ-calculus are untyped
λ-calculi extended with arbitrary linear combinations of terms. The former
presents the axioms of linear algebra in the form of a rewrite system, while
the latter uses equalities. When given by rewrites, algebraic λ-calculi are not
confluent unless further restrictions are added. Type systems can be used to
enforce confluence by ensuring strong normalisation, however in general either
they are too restrictive or introduce some non-classical elements such as
scalars in the types. In this work we provide a type system for the
linear-algebraic λ-calculus which is classical enough to allow an
interpretation in System F, while allow arbitrary linear combination of terms.
- 11h15-12h15 Simon Perdrix (joint work with Ali Assaf):
Completeness of algebraic CPS simulations.
- The algebraic lambda calculus and the linear algebraic
lambda calculus are two extensions of the classical lambda calculus with
linear combinations of terms. They arise independently in distinct
contexts: the former is a fragment of the differential lambda calculus, the
latter is a candidate lambda calculus for quantum computation. Their
operational semantics differ in the treatment of applications and algebraic
rules. We show how these two languages can simulate each other using an
algebraic extension of the well-known call-by-value and call-by-name CPS
translations. These simulations have been proven to be sound, in that they
preserve reductions. We prove that the simulations are also complete,
strengthening the connection between the two languages.
- 14h00-15h00 Marc Bagnol:
Espaces cohérents Quantiques, revisités.
- Les espaces cohérents quantiques ont été présentés par J.-Y Girard comme une
version "quantique" de ses espaces cohérents: la trame est remplacée par un
espace de Hilbert, les cliques par des opérateurs, etc.
La construction n'a pas été poussée très loin car elle ne passe pas à la
dimension infinie, nécessaire pour interpréter les exponentielles.
Cependant, la construction pourrait s'avérer utile comme modèle dénotationnel
du calcul quantique.
Je présenterai une version retravaillée des ECQ qui présentent de meilleures
propriétés "physiques" que les ECQ originaux.
- 15h00-17h00: Séance de travail et
discussions.
- 17h00-18h00 Phil Scott:
Towards a categorical GoI for MALLP.
- Séminaire exceptionnel de l'équipe LDP.