Semistructured data is an umbrella term encompassing data models which are not logically organized in tables (i.e., the relational data model) but rather in hierarchical structures using markers such as tags to separate semantic elements and data fields in a ‘self-describing' way. In this lecture we survey some of the multiple connections between formal language theory and semi-structured data, in particular concerning the XML format. We will cover ranked and unranked tree automata, and its connections to Monadic Second Order logic, First Order logic, and XPath. The aim is to take a glimpse at the landscape of closure properties, algorithms and expressiveness results for these formalisms.[-]

In this programmatic talk, we will sketch both a conceptual and formal framework for reasoning about the notion of algorithm. This framework will arise from the analysis we will make of the relationships existing between the notion of algorithm and other similar (but still different) notions, like that of computation and that of program. We will first show that the Turing-Church thesis concerning effective computability is not sufficient to capture the notion of algorithm, as it identifies programs which are intensionally different. We will then show the limits of the existing models of computation in capturing some basic construction processes that we are willing to call algorithmic. In order to solve this problem, we propose a formalisation of the notion of model of computation on the base of which we claim that the notion of algorithm could eventually be analyzed. This approach centered around the dynamics of program execution, reconciles the more mechanical view of computation (such as formalized by Turing machines and automata) with the logical view - as it in particular stems from a generalization of Jean-Yves Girard's Geometry of Interaction programme.[-]

Gentzen's sequent calculus can be given additional structure via focusing. We illustrate how that additional structure can be used to construct synthetic inference rules. In particular, bipolar formulas (a slight generalization of geometric formulas) can be converted to such synthetic rules once polarity is assigned to the atomic formulas and some logical connectives. Since there is some flexibility in the assignment of polarity, a given formula might yield several different synthetic rules. It is also the case that cut-elimination immediately holds for these new inference rules. Such conversion of bipolar axioms to inference rules can be done in classical and intuitionistic logics.
This talk is based in part on a paper in the Annals of Pure and Applied Logic co-authored with Sonia Marin, Elaine Pimentel, and Marco Volpe (2022).[-]

Semistructured data is an umbrella term encompassing data models which are not logically organized in tables (i.e., the relational data model) but rather in hierarchical structures using markers such as tags to separate semantic elements and data fields in a ‘self-describing' way. In this lecture we survey some of the multiple connections between formal language theory and semi-structured data, in particular concerning the XML format. We will cover ranked and unranked tree automata, and its connections to Monadic Second Order logic, First Order logic, and XPath. The aim is to take a glimpse at the landscape of closure properties, algorithms and expressiveness results for these formalisms.[-]

Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.[-]

Solving fixpoint equations is a recurring problem in several domains: the result of a dataflow analysis can be characterized as either a least or greatest fixpoint. It is well-known that bisimilarity - the largest bisimulation - admits a characterization as a greatest fixpoint and furthermore mu-calculus model-checking requires to solve systems of nested fixpoint equations.
Often, these fixpoint equations or equation systems are defined over powerset lattices, however in several applications - such as lattice-valued or real-valued mu-calculi - the lattice under consideration is not a powerset.
Hence we extend the notion of fixpoint games (or unfolding games, introduced by Venema) to games for equation systems over more general lattices. In particular continuous lattices admit a very elegant characterization of the solution.
We will also describe how to define progress measures which describe winning strategies for the existential players and explain how abstractions and up-to functions can be integrated into the framework.
(Joint work with Paolo Baldan, Tommaso Padoan, Christina Mika-Michalski) .[-]

The Quantified Constraint Satisfaction Problem (QCSP) is the generalization of the Constraint Satisfaction problem (CSP) where we are allowed to use both existential and universal quantifiers. Formally, the QCSP over a constraint language $\Gamma$ is the problem to evaluate a sentence of the form$$\forall x_{1} \exists y_{1} \forall x_{2} \exists y_{2} \ldots \forall x_{n} \exists y_{n}\left(R_{1}(\ldots) \wedge \ldots \wedge R_{s}(\ldots)\right),$$where $R_{1}, \ldots, R_{s}$ are relations from $\Gamma$. While CSP remains in NP for any $\Gamma, \operatorname{QCSP}(\Gamma)$ can be PSpace-hard, as witnessed by Quantified 3-Satisfiability or Quantified Graph 3Colouring. For many years there was a hope that for any constraint language the QCSP is either in P, NP-complete, or PSpace-complete. Moreover, a very simple conjecture describing the complexity of the QCSP was suggested by Hubie Chen. However, in 2018 together with Mirek Ol_ák and Barnaby Martin we discovered constraint languages for which the QCSP is coNP-complete, DP-complete, and even $\Theta_{2}^{P}$-complete, which refutes the Chen conjecture. Despite the fact that we described the complexity for each constraint language on a 3 -element domain with constants, we did not hope to obtain a complete classification.
This year I obtained several results that make me believe that such a classification is closer than it seems. First, I obtained an elementary proof of the PGP reduction, which allows to reduce the QCSP to the CSP. Second, I showed that there is a gap between $\Pi_{2}^{P}$ and PSpace, and found a criterion for the QCSP to be PSpace-hard. In the talk I will discuss the above and some other results.[-]