La première rencontre du projet se tiendra le mardi 8 juin 2010 au CIRM à Marseille.
Exposés
- 09h00-09h15 Lionel Vaux: Accueil.
- Exercice du port de la cravate.
- 09h15-10h00 Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson et Benoît Valiron: Equivalence of Algebraic λ-calculi.
- We examine the relationship between the algebraic λ-calculus (λ-alg) a fragment of the differential λ-calculus; and the linear-algebraic λ-calculus (λ-lin), 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 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, leading to a simulation 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.
- 10h00-10h45 Benoît Valiron: Quelque chose sur des questions dénotationelles pour le calcul algébrique.
- 10h45-11h00 Pause: café.
- 11h00-11h45 Alejandro Díaz-Caro et Barbara Petit: An additive type system for the linar-algebraic lambda-calculus.
- The linear-algebraic λ-calculus and the algebraic λ-calculus extend the λ-calculus allowing linear combinations of terms. A variant of these calculi provides sums of terms without coefficients (which nearly amounts to having natural numbers as coefficients). In fact, most calculi associated with differential linear logic are presented without coefficients. Thereby, the λ-calculus with sums becomes the most basic object of study.
We propose to study the role of sums within the linear-algebraic λ-calculus from a logical point of view. First we introduce an extension of System F with sum operator for types. Then we interpret it into a fragment of Linear Logic.
- 11h45-12h30 Michele Pagani: May and Must Solvability in the Resource Calculus.
- 12h30-14h00 Pause: repas au CIRM.
- 14h00-14h45 Thomas Ehrhard: A finiteness structure on resource terms.
- 14h45-15h30 Pablo Arrighi et Gilles Dowek: On the completeness of quantum computation models.
- The notion of computability is stable (i.e. independent of the choice of an indexing) over infinite-dimensional vector spaces provided they have a finite “tensorial dimension”. Such vector spaces with a finite tensorial dimension permit to define an absolute notion of completeness for quantum computation models and give a precise meaning to the Church-Turing thesis in the framework of quantum theory.
- 15h30-15h45 Pause: café.
- 15h45-16h30 Emmanuel Beffara: Algèbres d'ordres.
- On introduit un modèle quantitatif de l'interaction concurrente. Les objets élémentaires sont des combinaisons linéaires de relations d'ordre sur lesquelles agit un groupe de permutations qui représente le non-déterminisme potentiel lié à la synchronisation entre processus. La structure obtenue donne des modèles dénotationnels de calculs de processus standards, et les opérations sur les algèbres mènent (presque) à un modèle de la logique linéaire différentielle.
- 16h30-17h00 Clôture: conclusion et discussions.