Type theory and concurrency (Q1124322)

This very readable article discusses the use of an automated reasoning tool (Nuprl) in the context of concurrent programming, in particular Milner's CCS. To this end a denotational model of concurrency based on Aczel's non-well-founded sets is developed (which, by the way, resembles also de Bakker \& Zucker's processes approach, and) which serves as the basis for the implementation of CCS (and presumably also related calculi). The paper provides a short but excellent introduction to CCS and its semantics in terms of the model mentioned above, an overview of the Nuprl system, the implementation of the semantic model in Nuprl, and the Nuprl implementation of CCS and Hennessy-Milner logic.