Higher-Order and Symbolic Computation, 17(3)171
EditorialDavid Basin, Olivier Danvy, and Robert Harper
|
The present issue is composed of three contributed articles. In "Proving Correctness of Compiler Optimizations by Temporal Logic", David Lacey, Neil Jones, Eric Van Wyk, and Carl Christian Frederiksen present a way to specify and formally verify program transformations using a temporal logic, CTL-FV. They also establish the correctness of three common optimizations. Coloured Petri Nets are a high-level model of Petri nets in which tokens are not black dots as in Petri's original model, but carry some information. In "Implementing Coloured Petri Nets using a Functional Programming Language", Lars Michael Kristensen and Søren Christensen present the key algorithms and techniques underlying the Design/CPN tool. They also review cases studies of the practical use of Colored Petri Nets. In "A Retrospective on Region-Based Memory Management", Mads Tofte, Lars Birkedal, Martin Elsman, and Nils Hallenberg report on their experience in designing, implementing, proving correct, and assessing type and region based memory-management system for Standard ML. |
![[picture of journal cover]](../LISP.JPG)