Research activity in 2000
The research topic of the group is to build abstract models for reasoning about the semantics of programming languages, and then to develop formal tools, based on the semantics, for proving properties of programs. In particular, the semantics techniques are developed for paradigmatic languages, based on the lambda calculus, modeling different kinds of computation. The research activity of the group in 2000 follows essentially the line of using logical tools, developed using Linear Logic, for modeling properties of programs (inside both the TMR project "Linear Logic" and the progetto cofinanziato MURST "Logica Lineare e dintorni"). In [1] an experimental paradigmatic functional language for programming with P-TIME functions has been proposed. The language is designed from Intuitionistic Light Affine Logic, which is a restriction of Linear Logic . It can be typed automatically by a type inference algorithm that deduces polymorphic types à la ML.
In [2] a paradigmatic functional language for modelling different operational semantics has been proposed. The considered operational semantics include the call-by-name, the call-by-value and the lazy evaluation. A general notion of extensionality for this language has been defined, and it has been shown how this paradigmatic language can be used for proving semantics properties for a whole class of languages.
