Nominal Automata for Resource Usage Control
May 29th, 12.00
Aula F, Palazzo delle Scienze - Cagliari
Dipartimento di Informatica - Università di Pisa
Abstract. Two classes of nominal automata, namely Usage Automata (UAs) and Variable Finite Automata (VFAs) are considered to express resource control policies
over program execution traces expressed by a nominal calculus (Usages).
We first discuss some closure properties of UAs, and then show UAs less expressive than VFAs.
We finally carry over to VFAs the symbolic technique for model checking Usages against UAs, so making it possible to verify the compliance of a program with a larger class of security properties.
Differential Interaction Nets and True Concurrency
May 24th 15.00 & May 25th 14.00
Aula C, Palazzo delle Scienze - Cagliari
Laboratoire d'Informatique de Paris Nord, CNRS (France)
Abstract. Differential interaction nets have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. Their main novelty is the presence of non-determinism in the cut-elimination procedure. This allowed Ehrhard and Laurent to prove that standard process calculi (e.g., pi-calculus, solos calculus) can be encoded into differential nets. However, such techniques exploit an ad-hoc treatment of reduction, which is needed to guarantee the existence of a bisimulation.
In the first part of this talk (May 24th) we will introduce interaction nets, and then differential interaction nets as a special case. In the second part (May 25th), we will analyse differential nets from a "true concurrency" point of view (non-interleaving semantics, in particular based on event structures). We will see that differential nets are inherently less expressive than standard process calculi; we will then see how to enhance their expressivity.
Upcoming PhD course
Proofs and Types
May-June 2012Dipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari
Paolo Di Giamberardino
Dipartimento di Matematica e Informatica
Università degli Studi di Cagliari
Abstract. Computer science owes its birth largely to logic and to the research on the foundations of mathematics. In early nineties, the notion of "computational model" was defined in the framework of logic in order to give an answer to Hilbert's second problem: is there a general algorithm or mechanical procedure to establish, for each formula of arithmetic, whether it is a theorem or not, i.e. if the formula is deducible from the axioms?
Subsequentely, the theoretical notion of computational model was the basis on which modern computers were developed.
The "family resemblance" between logic and computer science was precisely formulated in the '60, with the discovery by Haskell Curry and William Howard of the isomorphism between proofs and programs, a cornerstone result connecting proof theory and programming languages.
The purpose of this short course is to present in an accessible way the Curry Howard isomorphism, highlighting its significance and importance.