|
Algebraic type systems| old_uid | 9529 |
|---|
| title | Algebraic type systems |
|---|
| start_date | 2011/01/17 |
|---|
| schedule | 15h30 |
|---|
| online | no |
|---|
| summary | In this talk I will present several extensions to the System F, for the sake of type the linear-algebraic lambda-calculus, a lambda-calculus enriched with a vectorial structure. The first type system is a straightforward extension of System F, which just types the calculus without any further adornment. The second one is a type system accounting for scalars, which can serve as a guarantee that the normal form of a term is of the form \sum a_i.t_i with \sum a_i=1. The following system includes "sums of types" reflecting that of the terms--showing that sums in the algebraic calculus behaves as a special kind of pairs. Eventually the last type system combines the previous two. We give counterexamples of why this kind of vectorial type system cannot be made in Curry style and show the clues of a future vectorial type system in Church style suitable to specialize the calculus into a quantum calculus. |
|---|
| responsibles | Poibeau |
|---|
| |
|