Delia Kesner's Festschrift

Program

09:10-09:30 Reception

09:30-10:30 Session 1

09:30-10:00 Beniamino Accattoli, Inria - École Polytechnique, France

The making of the linear substitution calculus and of tight multi types

The talk shall overview my joint works with Delia focussing on the inception of the ideas and the anecdotes behind the papers (rather than on the actual scientific content). Three main collaborations shall be discussed, the development of explicit substitutions at a distance, the quest for a standardization theorem for them, and the revisitation of de Carvalho's work about extracting quantitative information from intersection types.

10:00-10:30 Mariangiola Dezani, Università degli Studi di Torino, Turin, Italy

Sensible Intersection Type Theories

Finitary/static semantics in the form of intersection type assignments have become a paradigm for analysing the fine structure of all sorts of lambda models. The key step is the construction of a filter model isomorphic to a given lambda model. A property of great interest of filter models is  sensibility, i.e. the interpretation of all unsolvable terms in the same element.  The flexibility of intersection type assignments derives from their parametrisation on intersection type theories. In this talk intersection type theories are constructed as special meet-semilattices and appropriate morphisms, in the opposite category of meet-semilattices, are shown to preserve sensibility of the induced lambda models. Interestingly, the set of saturated sets together with the set of lambda terms is such a meet-semilattice, thus showing that arguments based on Tait-Girards's computability amount to the construction of a morphism. Two classes of intersection type theories which induce sensible filter models are characterised. The first class is non-effective, while the second is effective and it amounts to the generalisation of Mendler's criterion to intersection types and head normalising terms. The complete characterisation of sensible filter models however still escapes.

10:30-10:50 Coffee break

10:50-12:20 Session 2

10:50-11:50 Gabriele Vanoni, Université Paris Cité, France

Classical Duality and Relational Semantics
Joint work with Delia Kesner, Federico Olimpieri, and Daniel Ventura.

Denotational semantics of classical logic is a vast and active research area. The problem of finding the right notion of model is non-trivial because of the well-known result by Joyal, saying that any cartesian category with a dualizing object defines a Boolean algebra. We break the symmetry by exploiting Danos, Joinet, and Schellinx T/t and Q/q translations of classical logic into linear logic. In particular, we define two intersection/union type systems which are sound and complete for termination in the call-by-name and call-by-value fragments of Curien and Herbelin lambda-mu-mu-tilde sequent-style calculus. Then, from the type systems we extract the relational semantics.

11:20-11:50 Simona Ronchi Della Rocca, Dipartimento di Informatica, Università di Torino, Italy

From types to friendship

The presentation will be split into two sections. In the first section, I will reflect on my collaboration with Delia, highlighting the outcomes we achieved together (along with Antonio Bucciarelli) and how our friendship developed. In the second section, I will address some ongoing challenges I am currently tackling, alongside my collaborators.

11:50-12:20 Femke van Raamsdonk, VU University, Amsterdam, The Netherlands

Years with higher-order rewriting

I will share some memories related to Delia's work on higher-order rewriting.

12:20-14:00 Lunch break

14:00-15:30 Session 3

14:00-14:30 Val Tannen, Dept. of Computer and Information Science, University of Pennsylvania, USA

Incremental Evaluation of Algebraic Expressions

In databases, a useful paradigm, called incremental view maintenance, is applied when additional auxiliary information, called materialized views, is stored and used to optimize subsequent queries posed to the database. As the database is being updated, the changes need to be propagated to these materialized views. To do this efficiently we take advantage of the fact that views are defined by database queries and we might be able to avoid recomputing these queries on the entire updated database. Queries are usually described in algebras and this leads the title of this talk. 

We explore which algebraic varieties are subject to this form of efficient incremental change of query answers.

14:30-15:00 José Espírito Santo, Universidade do Minho, Braga, Portugal

Partial proof terms

Partial proof terms are proof terms where sequents occur as proper syntactic components, to represent “holes” or “gaps” in the structures generated by the proof search process. They are typed in logical systems extending ordinary proof systems with rules handling such partiality points; and we can define over them rewriting systems expressing proof search procedures. We apply these ideas to focusing (sequent calculus) and intercalation (natural deduction). Derivability in the original proof system becomes equivalent to normalizability in the rewriting system; and the two rewriting relations are, not only equivalent, but actually isomorphic. This is joint work with Ana Catarina Sousa.

15:00-15-30 Elaine Pimentel, Computer Science Department, University College London, UK

Between Classical and Constructive: Journeys with Delia in Proofs, Programs, and Friendship
In collaboration with Luiz Carlos Pereira, Mariana Milicich and Louis Riboulet.

Ecumenism can be understood as a pursuit of unity, where diverse thoughts, ideas, or points of view coexist harmoniously. In logic, ecumenical systems refer, in a broad sense, to proof systems for combining logics. One captivating area of research over the past few decades has been the exploration of seamlessly merging classical and intuitionistic connectives, allowing them to coexist peacefully.

In this talk, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz's seminal work. We will begin by elucidating Prawitz's concept of "ecumenism'' and present a pure natural deduction version of his system. We will then show how our ecumenical path crossed with Delia's, and how this encounter led us toward developing a term calculus for the implicational fragment of ecumenical logic.

This journey is not only about proofs and programs, but also about the joy of building ideas and friendships together.

15:30-16:00 Coffee break

16:00-17:00 Session 4

16:00-16:30 Mauricio Ayala-Rincón, Exact Sciences Institute, Universidade de Brasília, Brazil

Mechanizing substitutions for anti-unification

This talk will discuss current efforts to formalize substitutions for anti-unification procedures.

The presentation will consider the inspiring influence of Delia's work on reasoning on variable binding and substitutions.

16:30-17:00 Laurence Puel

Delia, her computer science history

I had the interesting opportunity to give a course at ESLAI, in Buenos Aires in 1988. Among the students, there was Delia. At the end of the course, she chose to continue her studies in Paris where I met her again. Later on, Delia wrote a thesis under my supervision. I would like to recall Delia's first years in Paris, then how she adopted  France and finally her attachment to Argentina where she was able to develop intense and durable cooperation between her two countries. I will show that during these almost 35 years, either for her personal research where she showed a very strong personality and has developed a dense activity with numerous cooperations or in her expert missions in our computer science community, Delia has always proceeded thoughtfully, honestly and listened to everyone. During all this time, Delia remained close to computer research in Argentina, developing successful projects for the benefit of both countries, leading to the creation of an international laboratory.

17:30-18:30 Closing toast