Type theory and concurrency
type: Item
instance of: scholarly article
title: Type theory and concurrency
zbMATH Open document ID: 0678.68017
DOI: 10.1007/BF01383954
author: Rance Cleaveland
author: Prakash Panangaden
published in: International Journal of Parallel Programming
publication date: 1988-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68N25
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 4111990
zbMATH Keywords: concurrency
zbMATH Keywords: type theory
zbMATH Keywords: denotational semantics
zbMATH Keywords: non-well-founded settheory
zbMATH Keywords: theorem proving
zbMATH Keywords: CCS
reviewed by: John-Jules Meyer
describes a project that uses: Nuprl
MaRDI profile type: Publication
cites work: Q3677160
cites work: Calculi for synchrony and asynchrony
cites work: A Theory of Communicating Sequential Processes
cites work: Q3777424
cites work: A calculus of communicating systems
cites work: Acceptance trees
cites work: Testing equivalences for processes
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Q3750136
cites work: Combinatory logic. With two sections by William Craig.
cites work: Q3997501
description: scientific article; zbMATH DE number 4111990