Evènement pour le groupe Séminaire Méthodes Formelles

Date 2016-10-25  11:00-12:00
TitreSemantics models for timed programing languages 
RésuméIn this talk, I consider temporally causal functions of timed streams, i.e. functions that produce output values at a given instant that only depends on the input values that have been received till that instant. Defining partial timed streams that form a directed complete partial order (DCPO), I will show how causal functions are nicely captured as limits of continuous and synchronous functions over these DCPO offering thus a denotational model of causal timed functions. Relaxing synchronous hypothesis to pre-synchronous hypothesis, I will show how every causal function admits a lattice of possible denotations such that: - the least element can be understood as the latest semantics of that function: output values are computed when they need to be outputted, - the greatest element can be understood as a the earliest semantics of that function: output values are computed as soon as all the input values they depend have been received. - other elements in between can be understood as the various possible computation schedules that can still be followed in order to run the causal function. The categorical properties of these continuous functions will then be detailed, offering various relevant operators for programing with these functions. Last, I will show that a notion of causal function residual is available so that a minimal (possibly continuous) IO-automaton can be associated to every causal functions, providing thus a clear operation (latest) semantics. Open perspectives or questions will conclude this presentation. 
OrateurDavid Janin 

Aucun document lié à cet événement.

Retour à l'index