An atomic cross-chain swap is a distributed coordination task where multiple parties exchange assets across multiple blockchains, for example, trading bitcoin for ether. An atomic swap protocol guarantees (1) if all parties conform to the protocol, then all swaps take place, (2) if some coalition deviates from the protocol, then no conforming party ends up worse off, and (3) no coalition has an incentive to deviate from the protocol. A cross-chain swap is modeled as a directed graph D, whose vertexes are parties and whose arcs are proposed asset transfers. For any pair (D,L), where D=(V,A) is a strongly-connected directed graph and L⊂V a feedback vertex set for D, we give an atomic cross-chain swap protocol for D, using a form of hashed timelock contracts, where the vertexes in L generate the hashlocked secrets. We show that no such protocol is possible if D is not strongly connected, or if D is strongly connected but L is not a feedback vertex set.

How does the Brain give rise to the Mind? How do neurons and synapses, molecules and genes, ​​evolution and development, give rise to behavior and cognition, language and intelligence? Despite lightning progress in recording and molecular technology and a deluge of experimental data, we do not seem to get closer to an answer. This is a talk about admiring and appreciating the problem, and proposing a new approach based on a recognized but little studied intermediate level of Brain computation carried out by the synchronous firing of large and highly interconnected sets of neurons called assemblies. We show that assemblies give rise to a novel computational system, and we speculate that they may instrument higher cognitive functions, such as language and math.

A dynamic graph algorithms is a data structure that maintains a property of a graph while it is modified by edge insertions and deletions. The last few years have seen exciting new developments in dynamic graph algorithms, namely strong conditional lower bounds and dynamic algorithm based on the primal-dual approach.

The undecidability of Hilbert's tenth problem (H10) about Diophantine equations turned out to be a powerful tool for establishing the undecidability of many other decision problems. The technique developed for proving the undecidability of H10 gave the possibility to find unexpected relationships between Diophantine equations and some other classical mathematical problems.

We revisit one of the most basic questions of database theory: the equivalence of first-order logic (FO), relational algebra (RA), and the core of SQL. Despite being at the heart of relational theory, these questions do not have satisfactory answers in the literature. The well known equivalence of FO and RA, and existing translations from SQL to RA, work only for simple models that fall short of what real databases use. Proving results about real SQL, rather than a theoretical reconstruction, is hampered by the lack of formal SQL semantics: the Standard is too vague for the purpose, and previous attempts at formalizing SQL's semantics made many simplifying assumptions that do not hold in real life. On the logic side, SQL mixes Boolean and 3-valued logics in a way that has never been properly studied.

Our goal is to fill these surprising gaps in basic database theory. We provide a formal semantics of the core of SQL that captures the real language and accounts for many of its idiosyncrasies. To justify it as the correct semantics, we validate it experimentally on a large number of randomly generated queries. With this semantics, we formally prove the equivalence of core SQL and RA, as well as the extension of 3-valued FO with an operator that accounts for SQL's ability to switch back and forth between Boolean and 3-valued logics. Then, somewhat surprisingly, we show that this additional operator does not add expressiveness, and - even more surprisingly - that 3-valued logic does not add expressiveness even in the presence of nulls.

Based on joint work with with Paolo Guagliardo.

Probabilistic programming is en vogue. It is used to describe complex Bayesian networks, quantum programs, security protocols and biological systems. Programming languages like C, C#, Java, Prolog, Scala, etc. all have their probabilistic version. Key features are random sampling and means to adjust distributions based on obtained information from measurements and system observations. We show some semantic intricacies, argue that termination is more involved than the halting problem, and discuss recursion and run-time analysis.

In software industry, engineers do formal logic day in and day out, even though they may not realize that. As a rule, they have not studied logic. Instead, they spent a lot of time studying calculus which they use rarely, if ever. I'll try to illustrate why logic is so relevant and why it is hard for software engineers to pick it up.

IMPORTANT NOTE: For administrative reasons, those from outside of IRIF who wish to attend the seminar in “Salle 3052” should email by Wednesday 26/10 their name to Irène Guessarian at ig@liafa.univ-paris-diderot.fr .

A vast amount of modern scientific and technological knowledge relies on the software that we have been collectively writing: deep knowledge from fields like mathematics, physics, chemistry, biology, medicine, finance and social sciences is now inextricably embodied into complex software systems, which model it at a level of detail that goes way beyond that of the usual scientific publications.

Preserving this software is of paramount importance to preserve our knowledge.

It is is a necessary prerequisite to allow the replication of experiments, which is the foundation of the scientific method, as well as to ensure our ability to modify and correct the software components that are constantly being incorporated into critical systems that need to stay in production for decades.

In this talk, we will review the challenges and opportunities we are facing, and discuss the role of Open Source as a key enabler.

The slides of the talk can be found here.

Ada Lovelace (born 200 years ago) wrote presciently about digital numerical calculations. She expressed its features poetically: “We may say most aptly that [Babbage's] Analytical Engine weaves algebraical patterns just as the Jacquard loom weaves flowers and leaves.” Ada explained the generality of digital computation, saying that “the engine can arrange and combine its numerical quantities exactly as if they were letters or any other general symbols.” We will discuss some of the expected and unexpected consequences of alternate representations of computational data. On the other hand, Ada wrote that “the engine [is] the material expression of any indefinite function of any degree of generality and complexity.” This we now know was overstating her case. We will discuss the formalization of the notion of effective computation and its consequences vis-a-vis computability and complexity of computation.