PhD Course: Bisimulation, process algebras, and coinduction

Lug 092012
 
Upcoming PhD course
Bisimulation, process algebras, and coinduction
July 2012
Dipartimento di Matematica e Informatica – Via Ospedale 72, Cagliari
Emilio Tuosto
Department of Computer Science
University of Leicester (UK)

Abstract. After a brief (non technical) introduction of the abstract concept of bisimulation, the course will show how this notion can be used to define observational semantics of concurrent computations expressed as process algebras (with names). Finally, the course will highlight the coinductive nature of bisimulation and how to use coinduction to reason about the behaviour of concurrent (or diverging) applications.

The
official presentation of the course will be on July 10 (Tuesday) in Aula Magna Matematica, at 18:00. The schedule of the course will be fixed during this
meeting.

Course schedule.

  • Tuesday 10, 18.00-19.00 Aula Magna Matematica
  • Thursday 12, 18.00-19.00 Aula C
  • Monday 16, 15.00-17.00 Aula C
  • Tuesday 17, 15.00-17.00 Aula C


The course has been funded by the Autonomous Region of Sardinia through the Visiting Professor Program 2011-12.

Seminar: Formal Models in Systems Biology

Lug 092012
 
Upcoming Seminar

Formal Models in Systems Biology

July 10, 16.00-18.00 Aula Magna Matematica,
July 12, 16.00-18.00 Aula C,
Palazzo delle Scienze – Cagliari


Andrea Bracciali
SICSA Lecturer – University of Stirling (UK)

Abstract. Papers
like "Protein molecules as computational elements in living cells"
[Bray, Nature 1995] and "Cells as computation" [Regev and Shapiro,
Nature 2002] have put forward the idea that many aspects of living
systems have a computational nature. Specifically, the complex network
of interaction and information exchange that occurs within the
biochemistry at the inter and intra cellular level, can be assimilated
to the functioning of a distributed, interactive computational system.
In the words of Bray, proteins are "functionally linked … into
biochemical 'circuits' that perform a variety of simple computational
tasks including amplification, integration and information storage".

Under
this perspective, it has appeared natural to employ the techniques used
to model and analyse interactive computational systems to the realm of
living organisms. Such a research trend aims at further developments
within Systems Biology, the research area that approaches the study of
the living organisms at a systemic level (see "Systems Biology: a brief
overview" [Kitano, Science 2002]). Computationally inspired formal
models and analysis techniques are being used to carry out "in silico"
experiments, which may often represent a cheaper, faster, more ethical,
more easily measurable, and less constrained complement to the more
traditional "in vitro/vivo" investigation.

This
extended-seminar will briefly survey some of the formal techniques,
particularly those originated from concurrency theory, which have been
adopted, adapted and further developed for the research in Systems
Biology. Starting from a historical perspective, the main ideas of the
approach will be discussed and a few small examples discussed.

The course has been funded by the Autonomous Region of Sardinia through the Visiting Professor Program 2011-12.
 Scritto da in 9 Luglio 2012  Senza categoria  Commenti disabilitati su Seminar: Formal Models in Systems Biology

Seminar: Nominal Automata for Resource Usage Control

Mag 282012
 
Upcoming Seminar


Nominal Automata for Resource Usage Control


May 29th, 12.00
Aula F, Palazzo delle Scienze – Cagliari

Pierpaolo Degano
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.
 Scritto da in 28 Maggio 2012  Senza categoria  Commenti disabilitati su Seminar: Nominal Automata for Resource Usage Control

Seminar: Differential Interaction Nets and True Concurrency

Mag 162012
 
Upcoming Seminar


Differential Interaction Nets and True Concurrency


May 24th 15.00 & May 25th 14.00
Aula C, Palazzo delle Scienze – Cagliari

Damiano Mazza
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.

PhD short course: Proofs and types

Apr 162012
 
Upcoming PhD course


Proofs and Types

May-June 2012

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


Contents.

  1. The simply-typed lambda-calculus (May 9, Aula F, 15:00-17.00)
  2. Intuitionistic logic and natural deduction. The Curry-Howard isomorphism (May 11, Aula F, 15:00-17.00)
  3. System F and polymorphism (June 22, Aula C, 12.00)


References.


  • J.Y. Girard, Y. Lafont, P. Taylor : Proofs and Types. Cambridge University, 1989.

  • L. Tortora di Falco: Sulla struttura logica del calcolo. Rendiconti di
    Matematica e delle sue applicazioni (vol. 26, serie VII – pagg.
    367-404), 2006.

Slides.
 Scritto da in 16 Aprile 2012  Senza categoria  Commenti disabilitati su PhD short course: Proofs and types
 Successivi
contatti | accessibilità Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929		 note legali | privacy