First day (August, 28th, altogether)

Schedule
9:00 - 9:30: Opening
9:30 - 11:00: lecture
11:00 - 11:30: coffee break
11:30 - 13:00: lecture
13:00 - 15:00: lunch
15:00 - 16:30: lecture
16:30 - 17:00: coffee break
17:00 - 18:30: lecture


Stefano Berardi (Università di Torino): Proofs as programs: the proof assistent Isabelle

Isabelle is an interactive theorem prover, which can be used to prove program properties by logical deductions, and to build tools that support and automate these deductions. Isabelle works through a dialogue between user and machine. The user describes the overall structure of the proof in a programming language-like notation. The system checks the correctness of each step and tries to fill in missing details. Link to the course page

School on Theoretical Computer Science (Aug. 29th - Sept. 1st)

lectures will start at 9:00 end end at 18:30 every day but on friday when they will end at 16:00

• Pierre Louis Curien (Université Paris VII e CNRS): Game semantics (Updated 12/9)

  Game semantics are denotational models of programming languages that are very precise, and in some cases even isomorphic to the syntactically constructed models. It has allowed to give a direct account of programming features such as references and control. The course will cover these fundamental aspects, as well as recent applications linking the subject with model-checking and abstract interpretation

• René David (Université de Savoie): Decidabilty results for primitive recursive algorithms

  The study of sequentiality is associated both with the game semantics of programming languages and with the full abstraction problem for PCF. After recalling the notion of sequential algorithms on concrete data structures introduced by Berry & Curien, I will show that these notions can give complexity and decidability results for primitive recursive algorithms. In particular, I will give an elementary proof of Colson's theorem on the complexity of computing the minimum of two integers and give some other results in this area

• Luca Paolini (Università di Torino): Semantics of PCF and the full abstraction problem (updated 12/9)

  PCF is a paradigmatic language, which has been historically used for studying the semantics of programming languages. The course introduces the syntax, the operational and the denotational semantics of the language PCF. The denotatonal semantics of the language will be presented both by using continuous functions of Scott and by using the stable functions of Berry. The problem of full abstraction problem will be taken into account. A model is fully abstract when the induced denotational semantics corresponds exactly to the operational one

School on Service-Oriented Architectures (Aug. 29th - Sept. 1st)

lectures will start at 14:00 on the first day, they will start at 9:30 from wednesday through friday; from wednesday through thursday they will end at 17:00 while on friday they will end at 12:30.

• Matteo Baldoni (Università di Torino): Web service conformance and interoperability

  One of the main challanges of the web, intended as a container of active resources (or services), is to enable the reuse of software, e.g. by allowing the automatic retrieval and composition of services, independently developed by different programmers. In this scenario it is important to have tools for verifying that a service conforms to a role specification in a given choreography and to guarantee that a set of services, separately proved conformant to the various roles of a choreography will actually be able to interoperate. Conformance and interoperability verificaton will be the topics of this lecture

• Giuseppe Berio (Università di Torino): Language engineering and MDA

  The lecture will present MDA and related elements (such as UML, MOF etc.). Then based on this introductory session, we will move to the problem of language engineering and possibly related areas such as domain specific languages. We then show some of the key mechanisms and apply them to one specific case (for instance SOA)

• Giovanna Petrone (Università di Torino): SOA and Web Services in the context of Enterprise Application Integration

  SOA and Web Services within the Enterprise Application Integration (EAI), starting with a brief history of the evolution of software architectures and middlewares starting from CORBA up to Web Services to reach the goal of interoperability. Web Services composition to realize workflow B2B, emerging standards like BPEL and others. At the end an introduction to choreography and conversationScuolaCollegno.tar.gz between Web Services as an application/evolution of Agents conversation

• Pierluigi Plebani (Politecnico di Milano): Quality of Web Service

  Web services nowadays available are usually described by their functional aspects according to WSDL and WS-BPEL specification. Actually, like any other software, Web services needs to be described in terms of non-functional aspects as well. The lecture aims at presenting the main issues related to Web service quality and the current models to describe and manage it

the published programs are subject to further adjustments