|
|
 |
|
Mardi 17 Février
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Problèmes de satisfaction de contraintes et graphes inhomogènes |
| Description: |
Élie de Panafieu |
Jeudi 19 Février
| Heure: |
16:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Modelling Timed Concurrent Systems Using Activity Diagram Patterns |
| Description: |
Étienne André UML is the de facto standard for modelling concurrent systems in the industry.
Activity diagrams allow designers to model workflows or business processes.
Unfortunately, their informal semantics prevents the use of automated verification techniques.
In this paper,
we first propose activity diagram patterns for modelling timed concurrent systems;
we then devise a modular mechanism to compose timed diagram fragments into a UML activity diagram that also allows for refinement, and
we formalise the semantics of our patterns using time Petri nets.
Our approach guides the modeller task% (helping to avoid common mistakes), and allows for automated verification.
Joint work with Christine Choppy and Thierry Noulamo |
Vendredi 20 Février
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Coherence spaces for computable analysis |
| Description: |
Kazushige Terui Abstract:
There have been two mainstream approaches in
computable analysis: the type-two theory of effectivity (TTE)
and the theory of domain representations. This paper proposes
an intermediary approach based on coherence spaces, which is
as concrete as TTE and as structured as domain theory.
We import various concepts from TTE such as admissibility,
and provide admissible representations for the real line, Euclidean
spaces and function spaces over them. This allows us
to represent, for instance, a real continuous function by a stable
map. A natural question is then what linear maps correspond
to in terms of analysis. Our answer is that they correspond
to uniformly continuous functions. This leads to an internal
expression of Heine's theorem (every continuous function on a
compact interval of the real line is uniformly continuous) as the
existence of a certain map from a stable function space to a linear
function space.
We finally illustrate an application of coherence spaces as a
type system for lambda calculus, which allows us to verify local
properties of real functions.
This is a joint work with Kei Matsumoto. |
|
|
