Type theory and concurrency (Q1124322)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Type theory and concurrency |
scientific article |
Statements
Type theory and concurrency (English)
0 references
1988
0 references
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.
0 references
concurrency
0 references
type theory
0 references
denotational semantics
0 references
non-well-founded settheory
0 references
theorem proving
0 references
CCS
0 references