Public iCal link: https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Seminars
Planning
Past seminars
Formalizing mathematics in Lean
Speaker: Floris van Doorn
Tuesday 9 November 2021, 11:00, (Salle des Thèses, bâtiment 650)
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.
Slides: here
Verified Software Components
Speaker: Murali Sitaraman, RESOLVE Research Group, School of Computing, Clemson University, USA
Monday 8 November 2021, 15:00, (online)
Abstract: This talk will summarize over three decades of programming language and software engineering research in the RESOLVE research group. The focus of the talk will be on building verified reusable software components. The talk will cover language design, software design, and verifier design to scale up automated verification of software correctness. Some of the discussion will be devoted to efforts on incorporating the ideas in computer science education and broadening participation in computing.
Reasoning over leaks of information for Access Control of Databases
Speaker: Pierre Bourhis, CRISTAL Lille
Tuesday 16 November 2021, 11:00, (Salle 1Z56, ENS Paris-Saclay)
Abstract: Controlling the Access of Data in Database management systems is a classical problem and it has been solved through different mechanisms. One of the most common implemented in most Databases management systems is the mechanism of views, i.e defining the accessible data of a user as the result of a query. This mechanism is also used in principle in other systems such as in social networks.
Unfortunately, this approach has some defaults. Even though it does not leak any secret information, the user seeing the data can infer some of these secret data by using different knowledge such as the logical definition of the query used to define the accessible data and different property of the database.
In this talk, I will present a formalism allowing to check when a set of views do not leak any information even through this kind of attacks.
Quantum simulation and causality
Speaker: Pablo Arnault, LMF
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
Speaker: Sébatien Bardin, CEA, Paris-Saclay
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
Speaker: Léon Gondelman, Aarhus University, DK
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
Speaker: Pierre Ohlmann, IRIF
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
Speaker: David Rudrauf
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...
Semantics for Variational Quantum Programming
Speaker: Vladimir Zamdzhiev, Inria/LORIA.
Tuesday March 15th 2022, 11:00, (online)
Abstract: In this talk, I will first introduce myself by briefly summarising my main research activities: (1) formal methods for diagrammatic reasoning about quantum information processing (e.g. higher-order rewriting of ZX-calculus diagrams); and (2) design and analysis of quantum programming languages. I will also explain how this fits perfectly within the research activities of the QuaCS team.
After that I will talk about some recent work on variational quantum programming that will appear in POPL 2022. The technical summary of this talk is below.
We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.