Forum Numerica - Logic, modalities and computation

In this talk, we will describe some aspects of logical systems that can be used in order to model some computational behaviours. We will start by briefly explaining what logical systems are, how proof systems can be built, and how we can relate such systems with computational models.

Then we will show how to capture different behaviours of distributed agents using logic. In order to do this kind of specification, it is often necessary to reason by using different types of modalities, such as time, space, or the epistemic state of agents. For instance, the access-control policies of a building might allow Bob to have access only in some pre-defined time, such as its opening hours. Another policy might also allow Bob to ask Alice who has higher credentials to grant him access to the building, or even specify that Bob has only access to some specific rooms of the building. Following this need, many formalisms have been proposed to specify, program and reason about such policies. Logic and proof theory have often inspired the design of many of these formalisms.

In this talk, we will show how to use linear logic with multi-modalities in order to reason about concurrent systems featuring different behaviours. This general approach has found application in different areas including the specification and verification of multimedia, access permissions and biochemical systems.

This will be an introductory talk, where we will assume no or little previous knowledge on the presented topics.

Elaine Pimentel is a full professor at the Federal University of Rio Grande do Norte (Brazil) and a researcher of the Brazilian’s research center CNPq. Her main research interests are proof theoretical aspects of logical systems and applications of logic to computational systems. She is currently in a sabbatical leave, working with Logic Groups at TU-Wien (Austria) and Inria (France).