Executable denotations for concurrent languages using Concurrent Transaction Logic
Marcus V. Santos · 2015
Abstract. This paper presents an approach based on a Horn fragment of Concurrent Transaction Logic ( CT R) for semantic description and execution of programming languages. The Horn notation is used in much the same way that plain Horn logic is used to specify semantics of programming languages. However, CT R extends that framework a deductive database language which provides a declara-tive, logic programming framework that naturally accommodates the notions of store, store updates, dataflow in declarative languages, data-driven concurrency, and message passing concurrency. The contributions of this paper are twofold: it shows how the semantics of concurrent programming lan-guages can be fully specified in a Horn-based logic framework; and it demonstrates that CT R-based logical denotations provide a unified formal semantics for such languages, which can also serve as a prototyping tool for the language developer.