My research activity is documented by the papers available on this site (also including some unpublished matherial) as well as on the DBLP archive.

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.

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.

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

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:

- S. Berardi, U. de'Liguoro: A Calculus of Realizers for EM1 Arithmetic. LNCS 5213: 215-229 (2008)
- S. Berardi, U. de'Liguoro: Toward the interpretation of non-constructive reasoning as non-monotonic learning. Inf. Comp. 207(1): 63-81 (2009)
- 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)
- S. Berardi, U. de'Liguoro: Knowledge Spaces and the Completeness of Learning Strategies, Proc. of CSL'12, LIPIcs 16, (2012)
- T. Coquand: A Semantics of Evidence for Classical Arithmetic. J. Symb. Log. 60(1): 325-337 (1995)
- E. M. Gold: Limiting recursion. J. of Symb. Log. 30:28-48 (1965)
- S. Berardi, U. de'Liguoro, Knowledge Spaces and the Completeness of Learning Strategies (full version), LMCS 10: 1-21 (2014)

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

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
*L _{A}* of all predicates of type

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

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

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