Higher-Order and Symbolic Computation, 15(1)5
EditorialOlivier Danvy, Takayasu Ito Tohoku and Carolyn Talcott
|
HOSC is starting 2002 with a substantially expanded advisory board. We
would like to warmly welcome the new members and to extend our thanks
to the old ones for continuing to serve HOSC. We would also like to
heartily welcome three new associate editors: David Basin, Andrzej
Filinski, and Julia Lawall. Like the other associate editors, they can
both identify relevant papers and manage the reviewing process. This
freedom and this responsability are parts of what makes HOSC both a
scholarly and collegial forum. The present issue is composed of three contributed articles. "Formalization and Analysis of Class Loading in Java" presents a soundness proof for the Java Virtual Machine using the Java2 loading constraint scheme and augmented value typing. "A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions" shows how to prove the completeness of an equational theory, using conversions to equate terms with the inverse of their semantic interpretation. "Dependent Types for Program Termination Verification" presents a framework for automatically verifying the termination of suitably annotated Dependent ML programs. |
![[picture of journal cover]](../LISP.JPG)