一句话：用类型系统刻画顺序性与良括号性，并给出比普通互模拟更粗的标号互模拟，证明其可靠性与受限完备性。
论文以 π 演算作为编程语言模型，指出其上下文允许任意并发，因而区分能力过强，会使一些在更规范上下文下应成立的行为等价失效。作者关注两种常见规范：顺序性，即任意时刻只有一个计算线程；良括号性，即对外部服务的调用遵循栈式纪律。文章用类型系统形式化这两种规范，并分别定义相应的标号互模拟。这些关系比普通互模拟更粗。作者证明它们相对于各自的上文 barbed 等价是可靠的，并在一定技术条件下是完备的。通过在函数表示与存储等例子上的应用，展示了该技术的有效性。
The $\pi$-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. In this paper we focus on two such common disciplines: sequentiality, meaning that at any time there is a single thread of computation, and well-bracketing, meaning that calls to external services obey a stack-like discipline. We formalise the disciplines by means of type systems. The main focus of the paper is on studying the consequence of the disciplines on behavioural equivalence. We define and study labelled bisimilarities for sequentiality and well-bracketing. These relations are coarser than ordinary bisimilarity. We prove that they are sound for the respective (contextual) barbed equivalence, and also complete under a certain technical condition. We show the usefulness of our techniques on a number of examples, that have mainly to do with the representation of functions and store.