文章基本信息

标题：Relational Reasoning about Contexts
本地全文：下载
作者：Søren B. Lassen
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1997
卷号：4
期号：24
出版社：Aarhus University
摘要：The syntactic nature of operational reasoning requires techniques to deal with term contexts, especially for reasoning about recursion. In this paper we study applicative bisimulation and a variant of Sands’ improvement theory for a small call-by-value functional language. We explore an indirect, relational approach for reasoning about contexts. It is inspired by Howe’s precise method for proving congruence of simulation orderings and by Pitts’ extension thereof for proving applicative bisimulation up to context. We illustrate this approach with proofs of the unwinding theorem and syntactic continuity and, more importantly, we establish analogues of Sangiorgi’s bisimulation up to context for applicative bisimulation and for improvement. Using these powerful bisimulation up to context techniques, we give concise operational proofs of recursion induction, the improvement theorem, and syntactic minimal invariance. Previous operational proofs of these results involve complex, explicit reasoning about contexts.