Theoretical Computer Science

Linear Logic and its applications to design and evaluation of functional programming languages.

If science is the pursuit of fundamental principles governing the world around us and the explanation of the phenomena we see, then you can define Theoretical Computer Science (TCS) as the "Science" at the base of computer science. The nature of TCS, formal and mathematical, is especially appropriate to provide the basics of the science of computation, given that computing itself is essentially a discrete logical process. In any case, it is clear that the theory is an essential part, integrated in almost everything we do today in computing and especially with the increasing links determined by the use of computers in everyday life and in other scientific disciplines.

The illustration of the central role of TCS in computer science, in terms of a large list of application opportunities and challenges to the theory and to its theorists in the 21th century has been described in various reports of the Association for Computing Machinery, one of the reference association which historically in the US and around the world collects the participation of a large number of researchers (particularly those of SIGACT - Special Interest Group Algorithms and Computation Theory). These reports describe the world of computing and its applications, and at the same time underline and illustrate the importance of the fundamental issues that are at the center of the discipline.

Although the role of the theory (and indeed of computing itself) can sometimes be used simply as a mean of promoting other sectors, the true role of the theory is to provide a direction of development, driving us while defining necessary models for the understanding of a problem and to get inspired in the innovation toward the exploration of new areas of application.


PELCR stands for Parallel Environment for optimal Lambda Calculus Reduction, it is part of a long term project to provide to the Functional Programming community an experimental environment to test different solutions to questions concerning parallel evaluation. An execution environment is conceived to run an infinite loop, think for instance to the fetch-decode-execute cycle in CPUs. We investigate in a formal setting the use of algebraic structures like ”streams” (introduced by J.J.M.M. Rutten - A coinductive calculus of streams) to give a formal description of a family of abstract machines implementing optimal reduction. Download PELCR on GitHub.

Mathematical foundations of this work come from Geometry of Interaction in Linear Logic; in particular, from the variant introduced in [DanosPediciniRegnier1994] and named Directed Virtual Reduction. From the point of view of implementation, abtract machines eventually allow to consider the quantitative model of parallel execution introduced by Leslie Valiant together to the execution environment PELCR introduced in [PediciniQuaglia2007].


Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre
Largo San Leonardo Murialdo 1, 00146 Rome - Italy


+39 06 57338519, fax: +39 06 57338340