Higher-Order and Symbolic Computation, 19(1)

The present issue is composed of four contributed articles on program analysis and transformation.

In "Semantics of Roundoff Error Propagation in Finite Precision Calculations", Matthieu Martel presents a theoretical tool to estimate the effect of roundoff errors on the accuracy of computations with finite precision. He introduces a symbolic perturbation ("first order error term") on the result of each floating point operation, and propagates it symbolically. The resulting semantics provides the basis for proving correctness of abstract interpretation-based analyzers involving floating-point arithmetics.

In "The Octagon Abstract Domain", Antoine Miné presents an abstract domain for the analysis of numerical properties and shows that this domain is a good compromise between precision and analysis costs to establish certain relationships among program variables. The implementation of the octagon domain is based on difference bound matrices.

In "Dynamic State Restoration Using Versioning Exceptions", Krishna Nandivada and Suresh Jagannathan present a new language construct called versioning exceptions where the program store is restored to its state prior to entering the handled block in which the versioned exception was raised, in the manner of Landin's J operator for control but for the state also. They present a static analysis for supporting the efficient implementation of versioned exceptions.

In "Polymorphic Typed Defunctionalization and Concretization", François Pottier and Nadji Gauthier present applications of a polymorphic lambda-calculus extended with guarded algebraic data types. They present a polymorphic version of John Reynolds's defunctionalization that is type-preserving, and a typed compilation of polymorphic records into basic records.