| Popis: |
University of Technology, Sydney. Faculty of Engineering and Information Technology. Ever since Milner showed that Church’s λ-calculus can be subsumed by π-calculus, process calculi have been expected to subsume sequential com-putation. However, Jay & Given-Wilson show that extensional sequential computation as represented by λ-calculus is subsumed by intensional se-quential computation characterised by pattern-matching as in SF-calculus. Given-Wilson, Gorla & Jay present a concurrent pattern calculus (CPC) that adapts sequential pattern-matching to symmetric pattern-unification in a process calculus. This dissertation proves that CPC subsumes both intensionality sequential computation and extensional concurrent computa-tion, respectively SF-calculus and π-calculus, to complete a computation square. A behavioural theory is developed for CPC that is then exploited to prove that CPC is more expressive than several representative sequential and concurrent calculi. As part of its greater expressive power, CPC provides a natural language to describe interactions involving information exchange. Augmenting the pattern-matching language bondi to implement CPC yields a Concurrent bondi that is able to support web services that exploit both sequential and concurrent intensionality. |
