APPSEM

Esprit Working Group 26142 - Applied Semantics

Final progress report

This is the final progress report for APPSEM, which ended on 31 March 2002 after a one year extension approved by the EC.

A proposal for a new Working Group APPSEM II is in preparation and will soon be submitted to the EC. The coordinator for this Working Group is Martin Hofmann, Ludwig-Maximilians-Universität, Munich, Germany.

APPSEM's objective: summary

Programming languages are the material from which every software product is built. They therefore have a huge economic impact: better programming languages will lead to higher programming productivity, reduced maintenance, and increased software reuse. Europe has great strength in programming language research, with many world leaders both in semantic theory and in implementation. The purpose of APPSEM is to bring these reseachers together in a Working Group, with the specific aim of improving the communication between theoreticians and practitioners. In this way we wish to focus theoreticians' attention on important practical problems as well as to speed up the application of new theoretical ideas in practice.

Applied Semantics Volume

To summarize some of the main achievements of APPSEM a volume based on the lecture notes from the International Summer School on Applied Semantics, Caminha, Portugal, 9-15 September 2000, will be published by Springer in the LNCS series as volume 2395. The preliminary lecture notes from the summer school have been revised and refereed before being accepted for inclusion in this volume which will appear shortly.

Spring School

The Spring School on Semantics of Programming Langugues was held in Agay-Var, near St Raphael in France, 24-29 March, 2002.

This spring school aimed at bringing together students and researchers eager to learn about the fundamental questions which language designers and implementors are facing today, and about the most up-to-date tools that theoreticians have developed or are in the process of developing (such as games and ludics, or realisability for classical logic and set theory).

Courses were held on the following subjects:

Security and security protocols
Classical realisability and new forms of control
Continuations, continuations-passing style and the CPS transformation
Quantitative semantics
Mobility in distributed systems
Ludics
Applications of realizability to objects and arithmetic
Compilation
Game semantics for imperative programs using regular languages
Types for information flow analysis

Workshops

APPSEM has promoted collaboration in the area by organizing and funding workshops and by funding travel between the APPSEM sites. During the final year the following workshops have been organizied

Second Symposium on Programs as Data Objects (PADO II), Aarhus, 21-23 May, 2001.
Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001), Siena, Italy, June 18-19, 2001.
Dependent Type Theory meets Practical Programming, Dagstuhl Seminar 01341, 19-24 August 2001.
Semantics, Applications and Implementation of Program Generation (SAIG'01), Firenze, 6 September 2001.
The 8th Biennial Workshop on Data Bases and Programming Languages (DBPL '01) Marino, Rome, 8-10 September 2001.

Symposium on Programs as Data Objects

This symposium brought together researchers working in the areas of programming and programming languages. The symposium focused on techniques and supporting theory for treating programs as data objects. Technical topics included:

Program manipulation: program specialization, type specialization, partial evaluation, normalization, reflection, rewriting, run-time code generation, self-application.
Program analysis: abstract interpretation, constraints, type inference, binding-time analysis.
Theoretical issues in representing and classifying programs: semantics, algorithmics, logics.
Applications: interpretation, compilation, compiler generation, verification, certification, meta-programming, instrumentation, incremental computation, staging, prototyping, debugging.

Mechanized Reasoning about Languages with Variable Binding

This workshop was about the use of computers to encode (operational) semantic descriptions of programming languages. Such encodings are often done within the metalanguage of a theorem prover or related system. The encodings may require the use of variable binding constructs, inductive definitions, coinductive definitions, and associated schemes of (co)recursion. The meeting was short, but highly focussed, and provided researchers with a forum to review state of the art results and techniques and to present recent and new progress in the areas of:

The automation of the metatheory of programming languages, particularly work which involves variable binding.
Theoretical and practical problems of encoding variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures.

Dependent Type Theory meets Practical Programming

The motivation of this Dagstuhl seminar was to bring together researchers from the communities of type theorists and of programming experts to discuss systems of dependent types. The seminar gave an opportunity for cross-fertilization of ideas, techniques and formalisms developed independently in these communities. In particular, the seminar aimed to make researchers in programming languages aware of new developments and research directions on the theory side; and to point out to theorists practical uses of advanced type systems and urge them to address theoretical problems arising in emerging applications.

Semantics, Applications and Implementation of Program Generation

This workshop was concerned with theoretical and practical models and tools for building program generators systems. Examples of topics included:

Semantics, type systems, and implementations for multi-stage languages.
Run-time specialization systems: e.g. compilers, operating systems.
High-level program generation (applications, foundations, environments).
Program synthesis from high-level specifications.
Symbolic computation, linking and explicit substitution, in-lining and macros.

Workshop on Data Bases and Programming Languages

This workshop aimed at promoting cross-fertilization between the fields Data Bases and Programming Languages.

Data Bases grew out of a separation between physical and logical data, thus enabling high level query languages. Data Base Query Languages have evolved in expressive power and structural capabilities. Programming Languages have seen a development from assembly languages to high level declarative paradigms. Thus the two areas approach each other as they mature. Earlier successful cross-fertilizations between the fields include the combination of relational theory, type theory and object-oriented languages, resulting in object-oriented data bases, object-relational data bases and persistent programming languages. The combination of databases logic programming and constraint programming produced deductive and constraint databases. Recently, with the emergence of semi-structured data models, there is a renewed synergy between databases and programming languages, in particular in the design of languages to manipulate XML data.

Visits between the sites

In addition to the networking costs for the workshops, APPSEM has funded about 25 visits by researchers from one APPSEM site to another during its final year.