Strong Normalisation in Higher-Order Action Calculi

Robin Milner

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The framework of action calculi accommodates a variety of disciplines of interaction and computation. A general theory of action calculi is under development; each particular action calculus — such as the π-calculus — will possess also a specific theory. It has previously been shown that any action calculus can be extended in a conservative manner to higher-order, thus allowing its actions to be encapsulated and treated as data. The dynamics of each higher-order calculus includes β-reduction, analogous to the λ-calculus. This paper demonstrates that under an assumption on the arities of a higher-order calculus (analogous to the assumption of simple types in the λ-calculus), β-reduction in higher-order action calculi is strongly normalising.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computer Software
PublisherSpringer Press
Number of pages19
ISBN (Print)978-3-540-63388-4, 978-3-540-69530-1
Publication statusPublished - 1997

Cite this