2015/03/15 by Nils Jähnig, Thomas Göthel, Sabine Glesner
Computer Science · #Action semantics #Computational semantics #Denotational semantics #Denotational semantics of the Actor model #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Normalisation by evaluation #Operational semantics #Semantics (computer science) #Well-founded semantics #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.178.2
published as EPTCS 178, 2015, pp. 9-21 · In Proceedings FESCA 2015, arXiv:1503.04378
openalex publication_date 2015/03/15 · arxiv created 2015/03/17 · arxiv updated 2015/03/18 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/31
An important property of programming language semantics is that they should be compositional. However, unstructured low-level code contains goto-like commands making it hard to define a semantics that is compositional. In this paper, we follow the ideas of Saabas and Uustalu to structure low-level code. This gives us the possibility to define a compositional denotational semantics based on least fixed points to allow for the use of inductive verification methods. We capture the semantics of communication using finite traces similar to the denotations of CSP. In addition, we examine properties of this semantics and give an example that demonstrates reasoning about communication and jumps. With this semantics, we lay the foundations for a proof calculus that captures both, the semantics of unstructured low-level code and communication.