Research work: an overview

My interests are to logic and computation. Central has been, and still remains, both pure and typed λ-calculus. Nonetheless, because of the emphasis on foundations of programming languages, I have also investigated other formalsims, like the ς-calculus and the π-calculus, partly related to λ-calculus.
My research activity is documented by the papers available on this site (also including some unpublished matherial) as well as on the DBLP archive and on ResearchGate.
Among my co-authors are: S. van Bakel, F. Barbanera, S. Berardi, M. Dezani, A. Piperno.

In this page I sketch some threads that I can figure out of my past and present work, pointing to the papers, of mines and by others, that I consider relevant.

Intersection types for λμ and related calculi

Control operatotors, especially handling continuations, have been added to λ-calculus by Felleisen and Parigot, though in different ways. This gives rise to extensions of the λ-calculus that can be used to realise non constructive proofs. The enhanced expressive power comes however at the price of dealing with caluli that are difficult to master.
Starting with a filter model construction of the continuation semantics in [7], an intersection type system has been devised in [2] and proved to be invaraint under subject conversion in Prigot's λμ-calculus, extending the construction in [1] for the λ-calculus. In [3] it has been shown that a suitable restriction of the system characterizes the strongly normalising λμ-terms (see [8] for a full paper including [2] and [3]). Finally in [4] the notion of extensional models of the Λμ-calculus from [5] (a variant of the models in [7]) has been studied w.r.t. the notion of approximation from [6], establishing the approximation theorem.

Bibliography

  1. H. Barendregt, M. Coppo, M. Dezani-Ciancaglini: A Filter Lambda Model and the Completeness of Type Assignment. J. Symb. Log. 48(4): 931-940 (1983)
  2. S. van Bakel, F. Barbanera, U. de'Liguoro: A Filter Model for λμ, Proc. of TLCA'11, LNCS 6690, 213-228 (2011)
  3. S. van Bakel, F. Barbanera, U. de'Liguoro: Characterisation of Strongly Normalising λμ-Terms, Post Proc. of ITRS'12, EPTCS 121: 1-17 (2013).
  4. U. de'Liguoro: The Approximation Theorem for the Λμ-Calculus, MSCS to appear.
  5. K. Nakazawa, S-y. Katsumata: Extensional Models of Untyped Lambda-mu Calculus. CL&C'12: 35-47 (2012)
  6. A. Saurin: Typing streams in the Λμ-calculus. ACM Trans. Comput. Log., 11(4), 2010.
  7. T. Streicher, B. Reus: Classical Logic, Continuation Semantics and Abstract Machines. J. Funct. Program. 8(6): 543-572 (1998)
  8. S. van Bakel: F. Barbanera, U. de'Liguoro, Intersection Types for the lambda-mu Calculus, unpublished (2014)

Proofs as learning strategies

Coquand's game theoretic interpretation of classical arithmetic [4] involves a sophisticated mechanism for withdrowing moves by the strategy that is supposed to defend a theorem established by non constructive means. Rather than to a game strategy, this is similar to a learning process, where the learner might discover to have been mistaken, and even to have been mistaken in beliving to have been mistaken, and so on. In this perspective Gold's idea of learning in the limit [5] can be extended to a more general theory, encompassing iterated limits but also allowing ingenuous learning strategies. This is the conetent of [2].
If only definite withdrow of guesses is allowed we have 1-backtracking and Gold's recursivenes in the limit. If not for the whole classical arithmetic, this is suffcient to interpret constructively primitive recursive arithmetic (PRA) extended by excluded middle of the form:
EM1: ∃x P ∨ ∀x ∼ P
where P is a primitive recursive predicate, possibly with parameters. In [1] the concept of interactive realizability is introduced, which are processes going through several stages of knowledge and learning by interacting with the "environment" and with each other. Interactive realizers are defined via λ-terms of the simply typed λ-calculus plus primitive recursion, and can be extracted from non constructive proofs in PRA-EM1 much as using Curry-Howard correspondence for intuitionistic proofs. A throughout study of the interpretation and the structuring of state dependent interpretation and interactive realizers will be found in [3]. To overcome the limitation on the logical complexity of the predicate P, in [4] the new concept of knowledge space has been introduced togather with a proper topology, leading to a more general concept of non-monotonic interactive realizability. [7] is the full version of [4].

Bibliography

  1. S. Berardi, U. de'Liguoro: A Calculus of Realizers for EM1 Arithmetic. LNCS 5213: 215-229 (2008)
  2. S. Berardi, U. de'Liguoro: Toward the interpretation of non-constructive reasoning as non-monotonic learning. Inf. Comp. 207(1): 63-81 (2009)
  3. S. Berardi, U. de'Liguoro: Interactive realizers. A new approach to program extraction from non constructive proofs. ACM Transactions on Computational Logic, 13 n. 2 (2012)
  4. S. Berardi, U. de'Liguoro: Knowledge Spaces and the Completeness of Learning Strategies, Proc. of CSL'12, LIPIcs 16, (2012)
  5. T. Coquand: A Semantics of Evidence for Classical Arithmetic. J. Symb. Log. 60(1): 325-337 (1995)
  6. E. M. Gold: Limiting recursion. J. of Symb. Log. 30:28-48 (1965)
  7. S. Berardi, U. de'Liguoro, Knowledge Spaces and the Completeness of Learning Strategies (full version), LMCS 10: 1-21 (2014)

Structuring communication via session types

Session types have been introduced in [5] as a tool for structuring communications (see [3] for more recent developments). A central role is played by a combination of  communication primitives with type assignment systems, ensuring correctness properties like error-freenes, but not stronger proprties like deadlock freenes and livenes. A step  toward that direction is the sty of Fellaisen's progress property in the context of concurrent systems like π-calculus, proposed in [2]. To increase expressiveness of session type systems Gay and Hole introduced subtyping for session types in [4]. This concept can be better understood modeling types as behaviours and subtyping a sub-behaviour relation, as it is done in [1] (see [6]) for the full version), where it emerges a fundamental asymmetry in the context of client/server service architecture.

Bibliography

  1. F. Barbanera, U. de'Liguoro: Two Notions of Sub-behaviour for Session-based Client/Server Systems. ACM SIGPLAN PPDP'10, 155-164 (2010)
  2. M. Dezani-Ciancaglini, U. de'Liguoro, N. Yoshida: On Progress for Structured Communications. LNCS 4912: 257-275 (2008)
  3. M. Dezani-Ciancaglini, U. de'Liguoro: Sessions and Session Types: an Overview. LNCS 6194: 1-28 (2010)
  4. S. Gay, M. Hole. Subtyping for Session Types in the Pi-Calculus. Acta Informatica, 42(2/3):191–225, 2005.
  5. K. Honda, V. Vasconcelos, M. Kubo: Language Primitives and Type Disciplines for Structured Communication-based Programming. LNCS 1381: 22–138 (1998)
  6. F. Barbanera, U. de'Liguoro: Sub-behaviour relations for session-based client/server systems, MSCS to appear (2014)

Logic semantics of object calculi

In Abadi and Cardelli's book [1] about the prototipical object calculus called ς-calculus, it is proposed an interpretation (below noted by ℑ(a)) of objects into the λ-calculus with records, which is credited to Kamin:
ℑ([li = ς(xi).bi, i ∈ I]) = ⟨ li = λ (xi).ℑ(bi), i ∈ I⟩
where ⟨ … ⟩ is just a record, so that the effect of the self binder ς(x) has to be achieved by means of record selection, λ-abstraction and self application:
ℑ(a.l) = (ℑ(a)⋅ l)ℑ(a) (where ⟨ … ⟩⋅ l represents the selection of the field labeled by l),
which is not typable in Church simply typed λ-calculus. Although it has a type in the intersection type discipline, so that relevant computational properties, e.g. convergence, can be characterized logically (see [4]).

The idea of logic semantics comes from filter models [3] and Abramsky's domain logic [2]. Roughly it amounts to say that the denotation of a program (say a λ-term) is the set of the properties derivable for it in some assignment system (e.g. intersection types). In [5] logical semantics is used to understand subtyping set-theoretically: let us suppose that "predicates" (just intersection types) can be assigned to typed terms, and that they are indexed by types, in the sense that to each type A it is associated a language LA of all predicates of type A. Then the way the typed equation t = t':A is undestood is: the set of predicates in LA that can be derived for t and for t' are the same. Now the subtyping judgment A <: B (A is a subtype of B) is roughly interpreted as LA ⊇ LB, which is consistent with the idea that the discriminating power of (the theory of) a type is the set of its predicates, and with the intuition that supertypes are less discriminating than their subtypes.

The approach, originally worked out for symply typed λ-calculus with records in [5], scales up to first order ς-calculus, giving a simple semantics to object and recursive types: see [6]. Moreover it has been extended to classes and mixins in [7].

Bibliography

  1. M. Abadi, L. Cardelli, A Theory of Objects. Springer-Verlag 1996
  2. S. Abramsky: Domain Theory in Logical Form. Ann. Pure Appl. Logic 51(1-2): 1-77 (1991)
  3. H. Barendregt, M. Coppo, M. Dezani: A Filter Lambda Model and the Completeness of Type Assignment. J. Symb. Log. 48(4): 931-940 (1983)
  4. U. de'Liguoro: Characterizing Convergent Terms in Object Calculi via Intersection Types. LNCS 2044: 315-328(2001)
  5. U. de'Liguoro: Subtyping in Logical Form. ENTCS 70 (2002)
  6. S. van Bakel, U. de'Liguoro: Logical Equivalence for Subtyping Object and Recursive Types. Theory Comput. Syst. 42(3): 306-348 (2008)
  7. U. de'Liguoro, T.-C. Chen: Semantic Types for Classes and Mixins, presented at ITRS'2014, (2014)

Non deterministic λ-calculi

In my PhD thesis I studied a non-deterministic extension of the type-free λ-calculus, and the results appeared in the work [1] with Piperno. To my knowledge Hennessy and Ashcroft [5] have been the first to consider erratic choice in the setting of λ-calculus:
M⊕N →M and M⊕N →N
Erratic choice can model non-deterministic processes, namely multivalued functions. Since however λ-terms might fail to reach a normal form, modeling the theory of a non deterministic λ-calculus naturally involves powerdomains. One can manage to avoid the technical intricacies of powerdomains by working in the category of continuous lattices; equivalently it is possible to build a filter model of such a calculus via the type assignment assignment of union and intersection types, originaly devised in [2] for pure λ-calculus. Indeed tha typing rule for M⊕N is:
M⊕N:σ ∨ τ if M :σ and N: τ
In [3] Boudol studies a λ-calculus extended by a parallel operator M||N, whose behaviour is given by the reduction rule:
(M||N)L → (ML)||(NL)
This is a restricted form of non determinism: M||N does not coummunicate internally, so that the parallel of two or more terms roughly represent the set of this terms, and eventually the set of values of the computation of a single initial term. The difference with erratic choice is that all the values are kept in parallel, and never discarded. Consequently the typing rule is:
M||N:σ ∧ τ if M :σ and N: τ
In [4] it is shown that this calculus, togather with call-by-name and call-by-value λ-abstractions, has a fully abstract model in the category of continuous lattices, which is described as a filter model built out of an assignemnt system of intersection and union types, plus the arrow and the universal type ω. In the model multiple values are interpreted into the join of the interpretations of the simple (say atomic) values, without resorting to powerdomain functors.

Bibliography

  1. U. de'Liguoro, A. Piperno: Nondeterministic Extensions of Untyped λ-Calculus, Inf. Comp. 122: 149-177 (1995)
  2. F. Barbanera, M. Dezani, U. de'Liguoro: Intersection and Union Types: Syntax and Semantics Inf. Comp. 119(2): 202-230 (1995)
  3. G. Boudol: Lambda-Calculi for (Strict) Parallel Functions Inf. Comput. 108(1): 51-127 (1994)
  4. M. Dezani, U. de'Liguoro, A. Piperno: A Filter Model for Concurrent lambda-Calculus. SIAM J. Comp. 27(5): 1376-1419 (1998)
  5. M. Hennessy, E. A. Ashcroft: A Mathematical Semantics for a Nondeterministic Typed lambda-Calculus. Theor. Comp. Sci. 11: 227-245 (1980)