A Denotational Semantics for Handel-C

11 years 4 months ago
A Denotational Semantics for Handel-C
We present a denotational semantics for a fully functional subset of the Handel-C hardware compilation language [1], based on the concept of typed assertion traces. We motivate the choice of semantic domains by illustrating the complexities of the behaviour of the language, paying particular attention to the prialt (priority-alternation) construct l-C. We then define the typed assertion traces over an abstract notion of actions, which we then instantiate as state-transformers. The denotational semantics is then given and some examples are discussed. As is fitting given those honoured at the Festschrift of which this paper is a part, we show how the work of both Dines Bj¨orner and Zhou Chaochen act as inspiration, from the past, into the future for this research work.
Andrew Butterfield
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Authors Andrew Butterfield
Comments (0)