Abstract. I will discuss the mathematical principle of equivariance: what is, why it's important, how it is consistent with the Axiom of Choice, and how this can be leveraged to improve practical applications of nominal techniques.

The talk will be based on this paper: https://arxiv.org/abs/1801.09443

https://academic.oup.com/logcom/article-abstract/30/2/525/5670601

Abstract. We present a style of algebra interpretations for many-sorted and higher-order term rewriting based on interpretations to tuples; intuitively, a term is mapped to a sequence of values identifying for instance its evaluation cost, size and perhaps other values of interest.

This gives a more fine-grained notion of the complexity of a term or TRS than notions such as runtime or derivational complexity, which is in particular useful to obtain complexity results for higher-order term rewriting systems.

Abstract. Rewriting theory is a well established model of computation equivalent to the Turing machines, and the most well known rewriting system is the λ-calculus. Confluence is an important and undecidable property related to the determinism of the computational process. Direct proofs of confluence are, in general, difficult to be done. Therefore, alternative characterizations of confluence can circumvent this difficulty for different contexts. This is the case of the so called Z property, which has been successfully used to prove confluence in several situations such as the λ-calculus with βη-reduction, extensions of the λ-calculus with explicit substitutions, the λμ-calculus, etc. In this work we present a

direct and constructive proof that the Z property implies confluence. In addition, we formalized our proof and an extension of the Z property, known as the Compositional Z, in the Coq proof assistant.

Abstract. Unification and its applications to verification of cryptographic protocols have been explored extensively. The main idea is that it is possible to reduce verification of protocols to solving symbolic equations between terms exchanged between Alice and Bob who follow a protocol for secure communication. This approach is further extended so that the terms are interpreted by taking into account the algebraic properties of function symbols that occur in them. For instance, properties such as associativity (A) and commutativity (C) occur frequently and AC-unification is used to verify protocols that employ AC function symbols. The underlying logical formalism for this whole approach is first-order logic with equality (i.e., equational logic). In this logic, the algebraic properties possessed by the function symbols are axioms of equational theories.

In this talk, I will present an overview of the recent results of our group. In particular, I will explain non-trivial modularity results when an equational theory is a non-disjoint union of other theories.

Abstract: The (untyped) lambda-calculus is an old topic, almost 90 years old. And yet—I’ll try to argue—its study is far from being over. The talk is a bird’s eye view of the questions I have worked on in the last few years: how to measure the complexity of lambda terms, how to decompose their evaluation, how to see their time cost via denotational semantics, and how all this varies according to the evaluation strategy. The talk aims at inducing a new way of looking at an old topic, focusing on high-level issues and perspectives. Also, it is an updated version of an invited talk given originally at FSCD 2019.

Abstract: In the 65th anniversary of the Logic Theory Machine (LTM), we pay homage to the early contributors of automated reasoning, by looking at some historical and technical aspects that laid the foundations of the field. The LTM, which is based on a Hilbert-style calculus for classical logic, was proposed and implemented by Newell and Simon in 1956, with subsequent improvements in the next few years. Despite the technical challenges, mostly imposed by the limited existing architectures at that time, and some methodological criticism, which we also intend to discuss, their approach has established some techniques and heuristics that have survived time and that are still in use today.

Abstract. Unification has several applications in computer science and mathematics: logic programming, theorem proving, type inference and so on. In this talk we revisit the problem of AC-unification, i.e., unification in the presence of associative-commutative function symbols. We talk about why this problem is harder than standard unification and give an example that illustrates Stickel and Fages' first-order AC-unification algorithm. Then, we discuss an interesting step of a structured proof of the algorithm completeness. To conclude, we discuss work in progress in formalising AC-unification in PVS as a first step to extend our work on nominal C-unification. This is joint work with Mauricio Ayala-Rincón, Maribel Fernández and Daniele Nantes-Sobrinho.

Abstract: In this talk we explore recent approaches to quantitative typing systems for programming languages with pattern matching features. Quantitative (non-idempotent intersection) types have been used to characterise solvability for a pair pattern calculus, in which a qualitative characterisation of head-normalisation was given by means of typability.

We show that one can go further and provide upper-bounds/exact measures for head-normalisation, by means of two resource aware quantitative type systems (system U and system E), which take advantage of specific technical tools. While system U provides upper bounds for the length of head-normalisation sequences and the size of normal forms, system E goes even further and produces exact measures for each of them, as well as discriminating between the different kind of reduction steps performed.

Abstract. In this talk, I will give a brief historical view of logics in AI, starting from the Dartmouth meeting where John McCarthy coined the term Artificial Intelligence, in 1956, passing through LISP and Prolog ("the AI programming languages") and arriving at the present days. I will explore some of the logics used for knowledge representation and their applications.