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

Date 2017-03-28  11:00-12:00
TitreTime domain (for time denotational semantics) 
RésuméDirected complete partial orders (cpos) are used in denotational semantics for describing the way each value is incrementally computed, passing from a completely unknown value to a completely known value. Then, continuous functions between cpos propagate increase of knowledge on their inputs to increase of knowledge on their outputs. In this talk, we define the notion timed cpo by means of a cut function that tells what part of any value is known before any given instant. In the induced partial order, the increase of knowledge explicitly refers to the passage of time. It follows that continuous functions between timed cpos provide denotational semantics model candidates for timed IO-system acting over (higher-order) time evolving values, e.g. timed streams, but also bounded below values, partial inductive structures, timed functions, etc. Definitions, examples and (closure) properties of these timed cpos and their continuous functions are provided throughout. 
OrateurDavid Janin 

Aucun document lié à cet événement.

Retour à l'index