Higher-Order and Symbolic Computation, 16(3)

Editorial

David Basin, Olivier Danvy, Julian Padget and Carolyn Talcott

The present issue is composed of three contributed articles.

"Formal Foundations of Operational Semantics" presents a formalization, using the PVS proof system, of a very general form of the CIU context lemma for higher-order languages with effects. The paper describes techniques for formalizing higher-order concepts such as variable binding that closely parallel informal reasoning. Several hidden assumptions in the original informal proof were discovered. The paper serves both as a roadmap for the full PVS axiomatization and proof script, and as a guide for developing further formal tools for reasoning about higher-order languages with effects.

"Comparing Parallel Functional Languages: Programming and Performance" presents a detailed evaluation of three state-of-the-art parallel functional languages: PMLS, GpH, and Eden. The authors consider both the different ways in which the three languages support communication and the specification and control of parallelism, as well as pure performance, by means of three applications: matrix multiplication, a linear-equation solver, and a ray tracer, executed on a Beowulf cluster. While moderate improvements result without changing the sequential code, tuning load distribution and thread granularity are shown to behighly beneficial.

"Strong Normalization from Weak Normalization" provides a systematic account of techniques for inferring strong normalization from weak normalization in the lambda-calculus. Common to all these techniques is the fact that they all use syntactic translations from lambda-terms to lambda-I-terms. The authors identify that all these translations can be factored through Klop's i translation and they provide in all cases the corresponding complementary translation. More generally, they show that all these translations are instances of Sørensen's permutative inner interpretations, and they present a detailed comparison of Gandy, Klop, and Girard's techniques for reducing strong normalization to weak normalization.

July 2003 - hosc@brics.dk