## Formalizing mathematics in Lean

Tuesday 9 November 2021, 11:00, (location to come)

**Abstract:** Lean's mathematical library mathlib is a rapidly growing unified library of formalized mathematics. The library contains a large part of an undergraduate math curriculum, many graduate topics, and some projects based on mathlib address more advanced topic I will give an overview of the design decisions in mathlib to make it suitable for formalizing mathematics, and some of the recent milestones in the library.

## Quantum simulation and causality

Tuesday 2 November 2021, 11:00, (amphi 1Z18, ENS Paris-Saclay)

**Abstract:** In the first part of my talk, I will show that quantum automata can be used to simulate the equations of the standard model of particle physics. These quantum automata are quantum circuits on a spacetime grid, satisfying two fundamental properties: they are reversible, as all equations of fundamental physics, and local, i.e., the information at one given node comes only from neighboring nodes, so that as in fundamental physics the speed of information is bounded by the speed of light. The equations that we are able to simulate go from quantum electrodynamics to quantum field theory in curved spacetime. In the second part of my talk, I will briefly talk about causal order in quantum theory and what I intend to investigate in this direction.

## Towards Security-Oriented Program analysis

Tuesday 7 September 2021, 11:00, (amphi 1Z53, ENS Paris-Saclay)

**Abstract:** While digital security concerns increase, we face both a urging demand for more and more code-level security analysis and a shortage of security experts. Hence the need for techniques and tools able to automate part of these code-level security analyses. As source-level program analysis and formal methods for safety-critical applications have made tremendous progress in the past decades, it is extremely tempting to adapt them from safety to security. Yet, security is not safety and, while still useful, a direct adaptation of safety-oriented program analysis to security scenarios remains limited in its scope. In this talk, we will argue for the need of security-oriented program analysis. We will first present some of the new challenges faced by formal methods and program analysis in the context of code-level security scenarios. For example, security-oriented code analysis is better performed at the binary level, the attacker must be taken into account and practical security properties deviate from standard reachability / invariance properties. Second, we will discuss some early results and achievements carried out within the BINSEC group at CEA LIST. Especially, we will show how techniques such as symbolic execution and SMT constraint solving can be tailored to a number of practical code-level security scenarios.

## Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic

Tuesday 15.6.2021, 11:00, online

**Abstract:** In this presentation we are going to talk about modular specification and
verification of causally-consistent distributed database, a data structure that
guarantees causal consistency among replicas of the database.

With causal consistency, different replicas can observe different data on the same key, yet it is guaranteed that all data are observed in a causally related order: if a node {$N$} observes an update {$X$} originating at node {$M$}, then node {$N$} must have also observed the effects of any other update {$Y$} that took place on node {$M$} before {$X$}. Causal consistency can, for instance, be used to ensure in a distributed messaging application that a reply to a message is never seen before the message itself.Read more...

## Controlling a random population

Tuesday 6.4.2021, 11:00, online

**Abstract:** Bertrand et al. introduced a model of parameterised systems,
where each agent is represented by a finite state system, and studied
the following control problem: for any number of agents, does there
exist a controller able to bring all agents to a target state? They
showed that the problem is decidable and EXPTIME-complete in the
adversarial setting, and posed as an open problem the stochastic
setting, where the agent is represented by a Markov decision process. In
this paper, we show that the stochastic control problem is decidable.
Our solution makes significant uses of well quasi orders, of the
max-flow min-cut theorem, and of the theory of regular cost functions.
We introduce an intermediate problem of independent interest called the
sequential flow problem, and study the complexity of solving it.

## Towards synthetic psychology: from phenomenology to cybernetics

Tuesday 9.3.2021, 11:00, online

**Abstract:**
The role of consciousness in biological cybernetics remains an
essential yet open question for science. We introduce the Projective
Consciousness Model (PCM) and show how its principles yield a unified
model of appraisal and social-affective perspective taking and a method
for active inference. We show how the PCM can account for known
relationships between appraisal and distance as an inverse distance law,
and how it can be generalised to implement Theory of Mind for strategic
action planning. We use simulations of artificial agents applied to toy
robots to demonstrate how different model parameters can generate a
variety of emergent adaptive and maladaptive behaviours: from the
ability to be resilient in the face of obstacles through imaginary
projections, to the emergence of social approach and joint attention
behaviours, and the ability to take advantage of false beliefs
attributed to others. The approach opens new paths towards a science of
consciousness, and applications, from clinical assessment to the design
of artificial (virtual and robotic) agents. We discuss the interest and
variety of computational challenges entailed by the approach. Read more...