ABSTRACT. This is a complete formalization of the work of Hoare and Roscoe on the denotational semantics of the Failure/Divergence Model of CSP. It follows essentially the presentation of CSP in Roscoe’s Book ”Theory and Practice of Concurrency” [8] and the semantic details in a joint Paper of Roscoe and Brooks ”An improved failures model for communicating processes". The present work is based on a prior formalization attempt, called HOL-CSP 1.0, done in 1997 by H. Tej and B. Wolff with the Isabelle proof technology available at that time. This work revealed minor, but omnipresent foundational errors in key concepts like the process invariant. The present version HOL-CSP profits from substantially improved libraries (notably HOLCF), improved automated proof techniques, and structured proof techniques in Isar and is substantially shorter but more complete.

ABSTRACT. The requirements for more advanced, longer, and more precise molecular dynamics simulations are greater than ever. Even though we are better at optimizing and have more computational power than previously, there is also a continuing need to make simulations even faster, more reliable, and cheaper to run. In this paper, we are presenting a method for running a molecular dynamics simulation on an FPGA device by using Synchronous Message Exchange. The molecular dynamics simulation presented in this paper is a basic simulation using the Lennard-Jones potential. It is a work in progress, but the results are promising compared to a Python implementation using matrix calculations. We present a proof of concept of an initial solution and its performance provides results that make us believe that a full molecular dynamics implementation would be feasible and competitive.

ABSTRACT. Occam is a programming language built on CSP, which has for many years been used for writing safety-critical systems used in space technology and at CERN among others. However, the language has not been developed or maintained for the last 25 years, which makes it difficult to maintain the programs which currently has a code base in Occam. As changing the entire code base for such systems will prove both expensive and time consuming, it is desirable to find an easy and secure way to translate Occam programs into another programming language. This paper lays the foundation of a transpiler from Occam to the newer programming language Go using Haskell. Go is a modern programming language which also implements many of the CSP principles found in Occam, making it a suitable target. The transpiler is implemented for a subset of Occam including only basic functionality, and is successful in translating simple programs from Occam to Go, showing that it is indeed possible to automatically translate Occam programs into Go.

ABSTRACT. Minor corrections and semantically valid restrictions, and one significant but equivalent change, allow the occam 2.0 syntax to be expressed in a yacc-compatible syntax (actually flex and bison are used) with very desirable properties. A rich 13-level descent structure (descent happens when a syntactic object is part of a definition of another syntactic object) is all singletons except for two levels (one equivalent to expression and the other equivalent to process), and these are broken up themselves into singletons by extended descent (parenthesis plus square bracket enclosure count, and indentation count, respectively). This will allow formal proofs of syntactic object behavior, and hence whole language behavior, to be vastly simplified.