An axiomatic semantics for the synchronous language Gentzen

Abstract

We propose an axiomatic semantics for the synchronous language Gentzen, which is an instantiation of the paradigm Timed Con- current Constraint Programming. We view Gentzen as a prototype of the class of state-oriented synchronous languages, since it offers the basic constructs that are shared by the languages in the class. Since synchronous concurrency cannot be simulated by arbitrary interleaving, we cannot exploit “head normal forms”, on which axiomatic theories for asynchronous process calculi are based.