### Thursday, May 20, 2021

**Florin Crăciun (Babeș-Bolyai University)
TBA
**

### Thursday, April 22, 2021

**Gabriel Istrate (West University of Timișoara)
Kernelization, Proof Complexity and Social Choice
**

**Abstract**: We display an application of the notions of kernelization and data reduction from parameterized complexity to proof complexity: Specifically, we show that the existence of data reduction rules for a parameterized problem having (a). a small-length reduction chain, and (b). small-size (extended) Frege proofs certifying the soundness of reduction steps implies the existence of subexponential size (extended) Frege proofs for propositional formalizations of the given problem. We apply our result to infer the existence of subexponential Frege and extended Frege proofs for a variety of problems. Improving earlier results of Aisenberg et al. (ICALP 2015), we show that propositional formulas expressing (a stronger form of) the Kneser-Lovasz Theorem have polynomial size Frege proofs for each constant value of the parameter $k$. Previously only quasipolynomial bounds were known (and only for the ordinary Kneser-Lovasz Theorem). Another notable application of our framework is to impossibility results in computational social choice: we show that, for any fixed number of agents, propositional translations of the Arrow and Gibbard-Satterthwaite impossibility theorems have subexponential size Frege proofs.

This is joint work with Cosmin Bonchiș and Adrian Crăciun.

### Thursday, April 15, 2021

**Dorel Lucanu
(Alexandru Ioan Cuza University of Iași)
(Co)Initial (Co)Algebra Semantics in Matching Logic
**

**Abstract**: Matching logic is a unifying foundational logic for defining formal programming language semantics, which adopts a minimalist design with few primitive constructs that are enough to express all properties within a variety of logical systems, including FOL, separation logic, (dependent) type systems, modal mu-logic, and more. In this presentation, we will show how the initial algebra semantics and the final (coinitial) coalgebra semantics are captured as theories in Matching Logic. The presentation will be examples-based.

This is joint work with Xiaohong Chen and Grigore Roșu.

References:

[1] X. Chen, D. Lucanu, G. Roșu. Matching logic explained. Journal of Logical and Algebraic Methods in Programming 120 (2021), 100638.

[1] X. Chen, D. Lucanu, G. Roșu. Initial algebra semantics in matching logic. UIUC Technical Report (2020).

### Thursday, March 11, 2021

**Mihai Prunescu (University of Bucharest)
Exponential Diophantine equations over ${\mathbb Q}$
**

**Abstract**: In a previous exposition [1] we have seen that the solvability over ${\mathbb Q}$ is undecidable for systems of exponential Diophantine equations. We now show that the solvability of individual exponential Diophantine equations is also undecidable, and this happens as well for some narrower families of exponential Diophantine equations.

References:

[1] M. Prunescu, The exponential Diophantine problem for ${\mathbb Q}$. The Journal of Symbolic Logic, Volume 85, Issue 2, 671-672, 2020.

### Thursday, March 4, 2021

**Pedro Pinto
(Technische Universität Darmstadt)
Unwinding of proofs
**

**Abstract**: The unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question: ``

*What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?*" This research program has since been dubbed proof mining and has been greatly developed during the last two decades and emerged as a new form of applied proof theory [1,2]. Through the use of proof-theoretical tools, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content from proofs that use infinitary noneffective principles. In this talk, we set out to give a brief introduction to the proof mining program, focusing on the following points:

- functional interpretations in an introductory way;
- the bounded functional interpretation [3,4];
- a concrete translation example: the metric projection argument.

References:

[1] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer, 2008.

[2] U. Kohlenbach. Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor, Proceedings of the International Congress of Mathematicians - Rio de Janeiro 2018, Vol. II: Invited lectures, pages 61-82. World Sci. Publ., 2019

[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135:73-112, 2005.

[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157:122-129, 2009.

[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. https://arxiv.org/abs/2101.12675, 2021.

[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.

### Thursday, February 25, 2021

**Horațiu Cheval (University of Bucharest)
Formalizing Gödel's System $T$ in Lean
**

**Abstract**: In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory, notably the program of proof mining. We give a brief overview of Gödel's system $T$ and then explore a formalization thereof as a deep embedding in the Lean proof assistant.

References:

[1] mathlib Community, The Lean Mathematical Library, 2019.

### Thursday, February 18, 2021

**Horațiu Cheval (University of Bucharest)
An introduction to Lean
**

**Abstract**: Lean is a proof assistant and programming language developed by Leonardo de Moura at Microsoft Research starting from 2013, based on dependent types and Coquand's Calculus of Inductive Constructions. It offers typical functional programming features, as well as a rich and extensible tactic language for writing proofs. The standard library, mathlib [1], implements an ever-increasing number of definitions and theorems, from basic facts about real numbers to more advanced topics like algebraic geometry or category theory, providing a structured framework for formalizing mathematics. We present an introduction to Lean's theory, methods of writing proofs and then look at how concrete mathematics is done in mathlib.

References:

[1] mathlib Community, The Lean Mathematical Library, 2019.

### Thursday, December 17, 2020

**Adriana Stancu (University of Bucharest)
Formal verification of SeL4
**

**Abstract**: This presentation introduces the SeL4 system, a microkernel first designed in Haskell, whose implementation in C has now a full formal proof of correctness. The focus is on the methods used to abstract the C code implementation into Isabelle/HOL theorems: syntactic translation, memory model and some abstraction levels added to refine the system representation, this involves usage of additional tools like a C-to-Isabelle parser and AutoCorres that will be shortly described.

References:

[1] G. Heiser, The seL4 Microkernel. An introduction. White paper, The seL4 Foundation, 2020.

**Adriana Stancu (University of Bucharest)
AutoCorres tutorial
**

**Abstract**: AutoCorres is a tool for abstracting C code into Isabelle/HOL (Isabelle's specialization in Higher Order Logic). This presentation will introduce some basic proof rules used in most of the Isabelle's theorems that will be needed to follow some introductory exercises of using AutoCorres tool with sample C programs. The study cases cover the following topics: proving correctness of programs with loops and proving statements about programs that manipulate heap memory.

References:

[1] D. Greenaway, Automated proof-producing abstraction of C code, PhD Thesis, University of New South Wales, Sidney, 2014.

### Thursday, December 3, 2020

**Andrei Sipoș (University of Bucharest / IMAR)
A quantitative multi-parameter mean ergodic theorem
**

**Abstract**: In [1], Avigad, Gerhardy and Towsner proof-theoretically analyzed the classical textbook proof due to Riesz of the mean ergodic theorem for Hilbert spaces in order to extract uniform rates of metastability. In [2], Kohlenbach and Leuștean extracted rates from a simplified argument of Garrett Birkhoff that applies to uniformly convex Banach spaces. What we do here [3] is to analyze another proof of Riesz which was inspired by Birkhoff's one and which delineates more clearly the role played by uniform convexity. The corresponding argument has the advantage that it can be used to prove a more general mean ergodic theorem for a finite family of commuting linear contracting operators.

References:

[1] J. Avigad, P. Gerhardy, H. Towsner, Local stability of ergodic averages. Trans. Amer. Math. Soc. 362, no. 1, 261-288, 2010.

[2] U. Kohlenbach, L. Leuștean, A quantitative mean ergodic theorem for uniformly convex Banach spaces. Ergodic Theory Dynam. Systems 29, 1907-1915, 2009.

[3] A. Sipoș, A quantitative multi-parameter mean ergodic theorem, arXiv:2008.03932 [math.DS], 2020.

### Thursday, November 5, 2020

**Andrei Sipoș (University of Bucharest / IMAR)
What proof mining is about
**

**Abstract**: Proof mining is an applied subfield of mathematical logic that aims to analyze proofs in mainstream mathematics using tools from proof theory. This area has been largely developed in the last couple of decades by the school of Ulrich Kohlenbach (see e.g. his monograph [1]). Here, I attempt to gently introduce the field to the working logician, by adapting my recent articles on The Proof Theory Blog [2,3].

References:

[1] U. Kohlenbach, Applied proof theory: Proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer, 2008.

[2] A. Sipoș, What proof mining is about, Part I, The Proof Theory Blog, 2020.

[3] A. Sipoș, What proof mining is about, Part II: Structures and metatheorems, The Proof Theory Blog, 2020.