TypiCal

Intervenant: Alejandro Díaz-Caro (LIG)

Date et lieu: 04/05, 14h, salle de réunion du préfabriqué du Lix

Résumé: The Linear-Algebraic Lambda-Calculus (arXiv:quant-ph/0612199) is a higher-order lambda-calculus together with the possibility to make linear combinations of terms. Terms can be seen as forming a vectorial space. However, dealing with concepts such as orthogonality and unitarity is not trivial. The scalar type system (arXiv:0903.3741) is a System F-like type system with scalars in the types. It can be seen as a first step towards a vectorial type system, with which to reason about orthogonality and unitarity. The additive type system is a type system with sums of types on it, which can be seen as a subset of the intuitionistic-multiplicative-exponential linear logic (IMELL). Finally, the vectorial type system puts scalar and additive together, making a vectorial space of types. In this seminar we will present these three type systems and some clues as to whether the last one enables us to check for orthogonality.

Liens: Les transparents de l'exposé.