Work Area: Logics and Logic Programming
Keywords abstract interpretation, partial evaluation, functional programming, declarative languages
Start Date: 24 July 92 / Duration: 36 months / Status: running
[ participants / contact ]
Abstract SEMANTIQUE is developing technology for manufacturing software under human guidance, but with minimal human involvement, with the aim of moving away from today's way of treating programs one-at-a-time to treating them as anonymous members of classes, subject to mechanical transformation, optimisation and other adaptations. Topics include abstract interpretation and partial evaluation.
The major goal of SEMANTIQUE is to establish, by a mixture of theoretical investigation and practical experiments, techniques which will allow the automation of the software manufacturing process. Topics of interest to members of the Group include semantic foundations of program analysis and manipulation, program analysis, program generation and advanced implementation techniques.
The Group's expertise ranges across a broad spectrum from pure theory through to extensive practical experience of implementing semantics-based program manipulation tools. Hitherto, the main emphasis of our work has been on the development of techniques for static analysis of programs based on abstract interpretation and program generation using partial evaluation. Over the last year, however, much of our work on program analysis has been based on non-standard type inference and we are beginning to look at other approaches to program generation (eg Turchin's notion of supercompilation). We have also devoted more effort on non-functional languages, for example analysis of CML (Concurrent ML) and partial evaluation of C. We have held our first major workshop, to which we invited a number of researchers from outside the Group. There have been a large number of short exchange visits.
Our progress and results fall into two categories: one methodological, the other concerning new applications.
Previous work on program analysis has emphasised the abstract interpretation approach. This work has been important for providing frameworks for correctness proofs and for understanding the relationships between different approaches. Unfortunately, the higher-order analyses have proved difficult to implement efficiently. Over the last two years, there has been a definite shift in our work to using non-standard type inference systems for describing analyses; the implementation route for such analyses has been well-studied. One tangible result of this work has been that the DIKU group have achieved a fourfold increase in speed for Similix by re-engineering the analyses to use constraint solving algorithms. We have developed several new analysis techniques for analysis of concurrent languages such as Linda, Gamma and Concurrent ML.
We are now considering other approaches to program generation, as well as partial evaluation. In particular, we have developed a deeper understanding of Turchin's notion of supercompilation and its relationship to partial evaluation. A partial evaluator for a large subset of the C programming language has been implemented; the Masters thesis reporting on this work was awarded a prize for the best Computer Science Masters Thesis in Denmark in 1992. This work has clear potential for industrial applications.
Semantics-based program analysis is at the interface between theory and practice. Since SEMANTIQUE is a Basic Research Working Group, the majority of our results take the form of scientific papers rather than artefacts. Nevertheless, our work on program generation is tested by means of prototype programs and the same is now true of our program analysis work in the context of the Glasgow Haskell Compiler. Similix and the Haskell compiler have been widely distributed. There are signs of growing industrial interest in the partial evaluation work and this will be promoted by the recent publication of Jones N D et al. (cited below).
In June 1993 the DIKU partner hosted the ACM Conference on Functional Programming Languages and Computer Architecture (FPCA'93), the ACM Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM'93), an IFIP Working Group meeting (WG 2.8 - Functional Languages) and a one-day workshop on state in Functional Programming Languages (SIPL). Hankin edited a special issue of the Journal of Logic and Computation devoted to Abstract Interpretation (August 1992) and Jones is editing a special issue of the Journal of Functional Programming devoted to Partial Evaluation.
Jones et al's book "Partial Evaluation and Automatic Program Generation" appeared in June 1993.
Imperial College of Science, Technology and Medicine - UK
Department of Computing
180 Queen's Gate
UK-LONDON SW7 2BZ
rhus University - DK
K_benhavns Universitet - DK
École Normale Supérieure - F
University of Glasgow - UK
Chalmers University - S
Dr. C. Hankin
tel +44/71 589 5111 ext. 5025
fax +44/71 581 8024
SEMANTIQUE - 6809, August 1994
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook