![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
Zena M. Ariola, Aaron Bohannon, and Amr Sabry. Sequent calculi and abstract machines.
https://www.cs.indiana.edu/~sabry/papers/sequent.pdf
The reductions corresponding to the abstract machine transitions must occur at a bounded depth from the root of the syntax tree.
Although languages based on lambda-calculi have been successful in supporting reasoning about high-level programs, in this paper we focus on sequent calculi. We show that sequent calculi are more suitable for reasoning about abstract machines since they allow one to define an evaluator for terms in a tail-recursive fashion, thus satisfying the above criterion.
https://www.cs.indiana.edu/~sabry/papers/sequent.pdf
The reductions corresponding to the abstract machine transitions must occur at a bounded depth from the root of the syntax tree.
Although languages based on lambda-calculi have been successful in supporting reasoning about high-level programs, in this paper we focus on sequent calculi. We show that sequent calculi are more suitable for reasoning about abstract machines since they allow one to define an evaluator for terms in a tail-recursive fashion, thus satisfying the above criterion.