Talks and slides
Intersection types for λμ and related calculi:
- Intersection types for -calculi with control
- Chocola, Lyon, France, October 1th 2015
We investigate -calculi extended with control operators from the point of view of intersection type theories.
Intersection types are a natural bridge between syntax and semantics and have been extensively used to characterize computational
properties of the untyped lambda-calculus. We aim at extending these techniques and results to calculi with control, whose semantics
is usually given either in terms of CPS translations or of abstract machines. Building over a denotational model of continuations
due to Streicher and Reus, that is a model of several such calculi, and using Abramsky's ideas on domain logic, we show how
type theories and type assignment systems can be obtained out of Streicher and Reus models as well as of the extensional
variant by Nakazawa and Katsumata, all inducing filter models in the sense of Barendregt-Coppo-Dezani.
- The Approximation Theorem for the -Calculus
- ICTCS 2013, Palermo, Italy, September 9th 2013
We consider a notion of approximation for terms of de Groote-Saurin -calculus.
Then we introduce an intersection type assignment system for that calculus which
is invariant under subject conversion. The type assignment system also induces a filter
model, which is an extensional -model in the sense of Nakazawa and Katsumata.
We then establish the approximation theorem, stating that a type can be assigned
to a term in the system if and only if it can be assigned to same of its approximations.
- Characterisation of Strongly Normalising -Terms
- ITRS 2012, Dubrovnik, Croatia, June 28th 2012
-calculus is provided by means of a typing system
with intersection and product types. The presence of the latter
ones (and of the type ) enables us to represent the
particular notion of continuation used in the literature for
defining the semantics of the -calculus. This allows
to lift to -terms the well-known characterisation
property for -terms possessed by the intersection types.
An interpretation of Parigot's propositional logical system into
ours will then provide an alternative proof of strong
normalisation for terms typeable in that system.
- A domain logic approach to Models of
and related calculi
- Domains X 2011, Swansea, UK, Sep 5th 2011
A revised version of the talk given at TLCA 2011.
- A Filter Model for the -Calculus
- TLCA 2011, Novi Sad, Serb Republic, June 1th 2011
- Abstract: We
introduce an intersection type assignment system for the pure -calculus,
which is invariant under subject reduction and expansion. The system is
obtained by describing Streicher and Reus's denotational model of
continuations in the category of -algebraic
lattices via Abramsky's domain logic approach. This provides a tool for
showing the completeness of the type assignment system with respect to
the continuation models via a filter model construction. We also show
that typed -terms have a
non-trivial intersection typing in our system.
Constructive interpretations of classical logic:
- Knowledge Spaces and Interactive Realizers
- CSL'12, September 6th 2012
We propose a theory of learning aimed to formalize some ideas underlying
Coquand's game semantics and Krivine's realizability of classical logic.
We introduce a notion of knowledge state together with a new topology,
capturing finite positive and negative information that guides a learning
strategy. We use a leading example to illustrate how non-constructive
proofs lead to continuous and effective learning strategies over knowledge
spaces, and prove that our learning semantics is sound and complete w.r.t.
classical truth, as it is the case for Coquand's and Krivine's approaches.
- Interactive realizers: a new approrach to program
extraction from non constructive proofs
- Genova, October 21th 2010
further elaborate the theory of interactive realizability, by defining
the categoy of individuals and strongly global functions.
- An interactive concept of integer and boolean to
model classical arithmetic constructively
- Types '09 - Aussois, France, May 13th 2009
We propose a realizability interpretation
of a system for quantiﬁer free arithmetic which is equivalent to the
fragment of classical arithmetic without nested quantiﬁers, which we
call EM1-arithmetic. We interpret classical proofs as interactive
learning strategies, namely as processes going through several stages
of knowledge and learning by interacting with the
with each other.
In this talk we give a categorical presentation of the model through
the construction of a suitable monad.
Types for processes:
- Session types for orchestrated interactions
(joint work with F. Barbanera)
- ICE'17 - Neuchatel, June 22-23, 2017
In the setting of the pi-calculus with binary sessions, we aim at relaxing the notion of duality of session types by the concept of retractable compliance developed in contract theory. This leads to extending session types with a new type operator of “speculative selection” including choices not necessarily offered by a compliant partner. We address the problem of selecting successful com- municating branches by means of an operational semantics based on orchestrators, which has been shown to be equivalent to the backtracking semantics of contracts, but clearly more feasible. A type system, sound with respect to such a semantics, is hence provided.
- A Game Interpretation of Retractable Contracts
(joint work with F. Barbanera)
- COORDINATION'16 - Heraklion, June 6-9, 2016
In the setting of contract theory, retractable contracts have been defined to formalize binary session protocols where the partners can go back to certain particular synchronization points when the session gets stuck, looking for a successful state, if any. In the present paper we propose a three-party game-theoretic interpretation of client/server systems of retractable contracts. In particular, we show that a client is retractable-compliant with a server if and only if there exists a winning strategy for a particular player in a game-theoretic model of contracts. Such a player can be looked at as a mediator, driving the choices in the retractable points. We show that winning strategies for the mediator player correspond to orchestrators in a system of orchestrated client/server sessions, and vice versa.
- Secure multiparty sessions with topics
(joint work with I. Castellani and M. Dezani)
- PLACES'16 - Eindhoven, April 8th, 2016
Multiparty session calculi have been recently equipped with security
requirements, in order to guarantee
properties such as access control
and leak freedom. However, the proposed security
requirements seem to be overly restrictive in some cases. In
particular, a party is not allowed to communicate any kind of public
information after receiving a secret information. This does not seem
justified in case the two pieces of information are totally
unrelated. The aim of the present paper is to overcome this
restriction, by designing a type discipline for a simple multiparty
session calculus, which classifies messages according to their
topics and allows unrestricted sequencing of messages on independent
- Global typing of local agents
- Seminar, Pisa, February 2013
- Abstract: We consider the
multi party schenario of non coordinated interacting agents as
initiated by Honda, Yoshida and Carbone, and illustrate the problem of
projectability of global type sepcifications into local session
Types for Client/Server Systems and their
behavioural semantics (joint work with F.
Barbanera, talk authored by Barbanera)
- Seminar, Reykjavik, Iceland, October 2010
We survey over session types for dyadic sessions and their
interpretation as contracts
of suitable kind.
- Two Notions
of Sub-behaviour for Session-based Client/Server Systems
- PPDP'10 - Hagenberg, Austria, July 27, 2010
We propose a
refinement and a simplification of the behavioural semantics of session
types, based on the concepts of compliance and sub-behaviour from the
theory of web contracts. We introduce two relations, representing the
idea of sub-behaviour from the point of view of the client and the
server, respectively, and characterize the sub-behaviour relation (from
the literature) as the intersection of the other two. We show that a
proper subclass of behaviours, called ``session behaviors'', and the
sub-behaviour relations model session types and subtyping, clarifying
the otherwise problematic extension of session type subtyping with
concepts from the theory of contracts.
Asymmetric Client-Server Interaction (joint work
with F. Barbanera and S. Capecchi; talk authored and given by S.
- FSEN'09 - Kish Island, Iran, April 15th 2009
We investigate client-server interaction where duties and rights of the
parties are asymmetric, in the sense that the client is allowed to
abort any session before the server has completed, but not vice versa.
This implies that the client can interact with any server offering at
least what she is looking for, but possibly more. We formalize such
asymmetry in the setting of session types via a form of subtyping in
depth, which we call prefix relation. This is apparently conflicting
with the rigid duality imposed by session types; nonetheless the
resulting system retains all basic correctness properties. Moreover,
the system we propose highlights interesting aspects concerning the
flow of communication inside a session. In particular it reveals that
usual subtyping theories cannot be extended by means of prefix, which
turns out to be a direrent concept.
- On Progress
- TGC'07 - Sophia Antipolis, France, October 6th 2007
propose a new typing system for the pi-calculus with sessions, which
ensures the progress property, i.e. once a session has been initiated,
typable processes will never starve at session channels. In the current
literature progress for session types has been guaranteed only in the
case of nested sessions, disallowing more than two session channels
interfered in a single thread. This was a severe restriction since many
structured communications need combinations of sessions. We overcome
this restriction by inferring the order of channel usage, but avoiding
any tagging of channels and names, neither explicit nor inferred. The
simplicity of the typing system essentially relies on the session
typing discipline, where sequencing and branching of communications are
already structured by types. The resulting typing enjoys a stronger
progress property than that one in the literature: it assures that for
each well typed process P which contains an open session there is a
well typed and irreducible process Q such that the parallel composition
P|Q always reduces, also in presence of interfered
Intersection types for object-oriented programming:
- Semantic Types for Classes and Mixins
- ITRS'14, Vienna, July 18, 2014
We consider a formalization of mixin composition and class linearization
yielding a class in mixin-based inheritance. We provide an interpretation
of the mixin calculus into a lambda-calculus extended with records and a record merge operator.
After extending the BCD intersection type assignment to such a calculus showing that types
are preserved by subject expansion and reduction, we naturally interpret mixin terms as
the sets of the types that can be deduced of their translations. It turns out that the class
obtained from a composition of mixins and the composition itself have the same logical meaning.
- A combinatorial view of module
composition for OO programming languages
- Dagstuhl Seminar 14232, Design and Synthesis from Components,
2 - 6 June 2014
Taking a lambda calculus with records as the basic model, we discuss
the choice of a set of combinators representing various possibilities
in composing software modules, designed as components to build class
hierarchies (e.g. traits or mixins).
We also consider a suitable extension of intersection type discipline
to be thought of as a specification language for module properties,
aiming at extending Rehof's method of program synthesis by inhabitation
to the case of class based programming languages.
object and recursive types logically
- ICTCS'05 - Pontignano (Siena), Italy, 12-14
- Abstract: Subtyping
in first order object calculi is studied with respect to the
logical semantics obtained by identifying terms that satisfy the same
set of predicates, as formalized through an assignment system. It is
shown that equality in the full first order sigma-calculus is modelled
by this notion, which on turn is included in a Morris style contextual
- Logical Semantics for the First Order
- ICTCS'03 - Bertinoro, Italy, 13-15 October 2003
- Abstract: We
investigate logical semantics of the first order sigma-calculus. An
assignment system of predicates to first order typed terms of the OB
calculus is introduced. We define retraction models for that calculus
and an interpretation of terms, types and predicates into such models.
The assignment system is then proved to be sound and complete w.r.t.
- Logical Semantics and PER Models
- CoMeta'02 - Venice, Italy, December 19-21, 2002
By using intersection types and filter models we formulate a theory of
subtyping via a finitary programming logic. Types are interpreted as
spaces of filters over a subset of the language of properties (the
intersection types) which describes the underlying type free
realizability structure. We show that such an interpretation coincides
with a PER semantics, proving that the quotient space arising from
``logical'' PERs taken with the intrinsic ordering is isomorphic to
the filter semantics of types. As a byproduct we obtain a semantic
proof of soundness of the logic semantics of terms and equation of a
typed lambda calculus with record subtyping.
- Characterizing convergent terms in object calculi
via intersection types
- TLCA'01 - Krakow, Poland, May 2-5, 2001
- Abstract: We
give a simple characterization of convergent terms in Abadi and
Cardelli untyped Object Calclulus (sigma-calculus) via intersection
types. We consider a -calculus
with records and its
intersection type assignment system. We prove that convergent
lambda-terms are characterized by their types. The characterization is
then inherited by the object calculus via self-application