Since 2014
Relational Reasoning about Contexts
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Relational Reasoning about Contexts
|
|
| Creator |
Lassen, Søren B.
|
|
| Description |
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.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1997-01-24
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18950
10.7146/brics.v4i24.18950 |
|
| Source |
BRICS Report Series; No 24 (1997): RS-24 Relational Reasoning about Contexts
BRICS Report Series; Nr. 24 (1997): RS-24 Relational Reasoning about Contexts 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18950/16589
|
|