|
Full Abstraction for Resource Calculus with Tests| old_uid | 9286 |
|---|
| title | Full Abstraction for Resource Calculus with Tests |
|---|
| start_date | 2010/11/22 |
|---|
| schedule | 15h30-16h30 |
|---|
| online | no |
|---|
| summary | In this seminar we present a fully abstract model of the resource calculus "with tests".
We will first shortly recall the full resource calculus à la Tranquilli together with its relational model D, and we will define the problem of full-abstraction in this context.
We will then show that D is also a model of a resource calculus extended with two unary operators (similar to "raise" and "catch" of programming languages) and parallel composition |. With these operators (arising from differential proofnets) we can define "tests" that are able to check whether a term of the resource calculus converge.
We will then associate each element sigma in the interpretation of a term M with a context C_sigma converging on M and diverging on terms "different" from M. This will give us the full abstraction result. |
|---|
| responsibles | Poibeau |
|---|
| |
|