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

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].