Talks and slides

Intersection types for $\lambda$-calculi with control and effects:

From semantics to types: the case of the imperative $\lambda$-calculus (joint work with R. Treglia)

MFPS'21 - Salzburg, Austria, August  31th, 2021

Abstract:  We propose an intersection type system for an imperative $\lambda$-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is derived by solving a suitable domain equation in the category of $\omega$-algebraic lattices; the solution consists of a filter-model generalizing the well known construction for ordinary $\lambda$-calculus. Then the type system is obtained out of the term interpretations into the filter-model itself. The so obtained type system satisfies the "type-semantics" property, and it is sound and complete by construction.

[pdf] [video]

On the reduction of the type-free computational $\lambda$-calculus (joint work with R. Treglia, author of the slides)

IWC'20 - Paris, France, June  30th, 2020

Abstract:  We study the reduction of the computational $\lambda$-calculus in the untyped case. To this aim, we consider a minimal fragment of the $\lambda$-calculus with monads as introduced by Wadler, and define a notion of call-by-value reduction just by orienting the three monad equational laws. We then prove confluence of its compatible closure. Finally, we show factorization of any reduction sequence into essential and inessential steps.

[pdf]

Intersection Types for the Computational $\lambda$-Calculus

INRIA - Sophia Antipolis, France, December  17th 2019

Abstract:  We study polymorphic type assignment systems for untyped $\lambda$-calculi with effects. We first introduce the type-free computational $\lambda$-calculus where a generic monad T is considered, whose syntax and reduction derive from semantics, and more precisely the call-by-value equation $$D = D → TD by Moggi, and Wadler's presentation of monads for Haskell. Then we introduce an intersection type assignment system in the style of Barendregt, Coppo and Dezani's system for ordinary $\lambda$-calculus. We establish subject reduction and expansion properties, as well as soundness and completeness w.r.t. a natural type interpretation. Further we establish the computational adequacy of the filter model via a characterization theorem of convergent terms. Finally we discuss how to extend the semantics to the case of specific monads, and show a result on what we call "monadic type interpretations".

[pdf]

The Approximation Theorem for the $\Lambda \mu$-Calculus

ICTCS 2013, Palermo, Italy, September  9th 2013

Abstract:  We consider a notion of approximation for terms of de Groote-Saurin $\Lambda \mu$-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 $\Lambda \mu$-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.

[pdf]

Characterisation of Strongly Normalising $\lambda \mu$-Terms

ITRS 2012, Dubrovnik, Croatia, June  28th 2012

Abstract:  $\lambda \mu$-calculus is provided by means of a typing system with intersection and product types. The presence of the latter ones (and of the type $\omega$) enables us to represent the particular notion of continuation used in the literature for defining the semantics of the $\lambda \mu$-calculus. This allows to lift to $\lambda \mu$-terms the well-known characterisation property for $\lambda$-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.

[pdf]

A domain logic approach to Models of $\lambda \mu$ and related calculi

Domains X 2011, Swansea, UK, Sep  5th 2011

Abstract:  A revised version of the talk given at TLCA 2011.

[pdf]

A Filter Model for the $\lambda \mu$-Calculus

TLCA 2011, Novi Sad, Serb Republic, June  1th 2011

Abstract:  We introduce an intersection type assignment system for the pure $\lambda \mu$-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 $\omega$-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 $\lambda \mu$-terms have a non-trivial intersection typing in our system.

[pdf]

Constructive interpretations of classical logic:

Knowledge Spaces and Interactive Realizers

CSL'12, September 6th 2012

Abstract:  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.

[pdf]

Interactive realizers: a new approrach to program extraction from non constructive proofs

Genova, October 21th 2010

Abstract:  We further elaborate the theory of interactive realizability, by defining the categoy of individuals and strongly global functions.

[pdf]

An interactive concept of integer and boolean to model classical arithmetic constructively

Types '09 - Aussois, France, May 13th 2009

Abstract:  We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, 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 “environment” and with each other. In this talk we give a categorical presentation of the model through the construction of a suitable monad.

[pdf]

Types for processes:

Partecipants as interfaces for composing open systems  (based on joint work with F. Barbanera and R. Hennicker)

BehAPI - Buenos Aires, February 16, 2023

Abstract: We propose a novel connection mechanism such that interface CFSMs are replaced by automatically generated “gateway” CFSMs, enabling messages to be exchanged between the systems. As a crucial outcome of our approach we prove that, under mild assumptions, if CFSM systems are connected in such a way a number of important communicating properties is preserved: deadlock-freeness, strong deadlock-freeness, orphan-message freeness, freeness of unspecified receptions, and progress.

[pdf]

Towards Refinable Choreographies  (joint work with H. Melgratti, E. Tuosto)

ICE - Valletta, Malta, June 19, 2020

Abstract: We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, that is the sufficient conditions that guarantee a protocol to be implementable. We introduce a typing discipline that enforces well-formedness of typed choreographies. Then we unveil the relation among refinable choregraphies and their admissible refinements in terms of an axiom scheme.

[pdf] [video]

Mailbox Types for Unordered Interactions  (joint work with L.Padovani)

BehAPI - Buenos Aires, February 26, 2019

Abstract: We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous pi-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.

[pdf]

Mailbox Types for Unordered Interactions  (joint work with L.Padovani)

Types'18 - Braga, June 18-21, 2018

Abstract: Preliminary version of the talk in Buenos Aires.

[pdf]

Session types for orchestrated interactions  (joint work with F. Barbanera)

ICE'17 - Neuchatel, June 22-23, 2017

Abstract: 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.   

[pdf]

A Game Interpretation of Retractable Contracts  (joint work with F. Barbanera)

COORDINATION'16 - Heraklion, June 6-9, 2016

Abstract: 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.   

[pdf]

Secure multiparty sessions with topics  (joint work with I. Castellani and M. Dezani)

PLACES'16 - Eindhoven, April 8th, 2016

Abstract: 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 topics.   

[pdf]

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.  

[pdf]

Session Types for Client/Server Systems and their behavioural semantics (joint work with F. Barbanera, talk authored by Barbanera)

Seminar, Reykjavik, Iceland, October 2010

Abstract: We survey over session types for dyadic sessions and their interpretation as contracts of suitable kind.

[pdf]

Two Notions of Sub-behaviour for Session-based Client/Server Systems

PPDP'10 - Hagenberg, Austria, July 27, 2010

Abstract: 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.

[pdf]

Typing Asymmetric Client-Server Interaction (joint work with F. Barbanera and S. Capecchi; talk authored and given by S. Capecchi)

FSEN'09 - Kish Island, Iran, April 15th 2009

Abstract: 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.

[pdf]

On Progress for Structured Communications

TGC'07 - Sophia Antipolis, France, October 6th 2007

Abstract: We 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 sessions.

[pdf]

Intersection types for object-oriented programming:

Semantic Types for Classes and Mixins

ITRS'14, Vienna, July 18, 2014

Abstract:  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.

[pdf]

A combinatorial view of module composition for OO programming languages

Dagstuhl Seminar 14232, Design and Synthesis from Components, 2 - 6 June 2014

Abstract:  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.

[pdf]

Subtyping object and recursive types logically 

ICTCS'05 - Pontignano (Siena), Italy, 12-14 October 2005

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

[pdf]

Logical Semantics for the First Order Sigma-Calculus 

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. retraction models.

[pdf]

Logical Semantics and PER Models 

CoMeta'02 -  Venice, Italy, December 19-21, 2002

Abstract:  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.

[pdf]

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 $\lambda$-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 interpretation.

[pdf]