In spite of the COVID-19 outbreak, we are glad to host BCTCS 2020 starting today, even if virtually. For more information on invited and contributed talks, check the official BCTCS 2020 website.

# Category Archives: Event

# Seminar series on Computability Theory and its Applications

Our colleague Arno Pauly is on the Programme Committee of the Computability Theory and its Applications seminar series, which currently is taking place virtually.

The seminar now has a YouTube channel where you can find the recordings of past talks you may have missed. The information on future talks, the timings of those, and the links to the videos are all available on the webpage here:

# 2nd World Logic Day

Today as a part of the 2nd World Logic Day our Theory group commemorated the work of Erik Palmgren (1963-2019), who sadly passed away last year.

Anton Setzer presented Erik’s most influential papers, which had a big impact on Anton’s own research.

# Meeting to commemorate the logician Erik Palmgren (1963-2019) on the occasion of the World Logic Day

We meet to remember the great logician Erik Palmgren who sadly passed away in November 2019 .

To honor Erik Palmgren’s work, Anton Setzer will give a talk with the title:

*Palmgren’s interpretation of inductive definitions in type theory and development of higher type universes in type theory.*

The meeting also marks the 2nd World Logic Day.

Venue: Theory Lab (CoFo 209)

Time: 14th of January 2020, 2-3 pm

# 2nd Proof Society Workshop on Proof Theory and its Applications

Following the Summer School, we are really proud to host the 2nd Proof Society Workshop. The workshop was an opportunity to listen to a lot of interesting invited and contributed talks on proof theory and various areas of its application:

**Adam Wyner:** Computational Law – The Case of Autonomous Vehicles

**Yong Cheng:** Exploring the incompleteness phenomenon

**Matthias Baaz:** Towards a Proof Theory for Henkin Quantifiers

**Sonia Marin:** On cut-elimination for non-wellfounded proofs: the case of PDL

**Gilles Dowek:** Logical frameworks, reverse mathematics, and formal proofs translation

**Benjamin Ralph:** What is a combinatorial proof system?

**William Stirton:** Ordinal assignments correlated with notions of reduction

**Oliver Kullmann:** Practical proof theory: practical versions of Extended Resolution

**Anton Setzer** and** Ulrich Berger **on behalf of **Ralph Matthes:** Martin Hofmann’s case for non-strictly positive data types – reloaded

**Laura Crosilla:** Philosophy of mathematics and proof theory

**Takako Nemoto:** Recursion Theory in Constructive Mathematics

**Arno Pauly:** Combinatorial principles equivalent to weak induction

**Antonina Kolokolova:** The proof complexity of reasoning over richer domains

**Joost Joosten:** The reduction property revisited

**Helmut Schwichtenberg:** Computational content of proofs

Thanks to all the speaker and participants and we hope to see you all again soon.

# Summer School: Day 4

Congratulations to Iris van der Giessen for winning the best poster competition and special thanks to Andreas Weiermann for the beautiful picture of Wales that serves as our main prize.

Big thanks to all the speakers and the participants for joining our Summer School. We hope to see you again during the future events by the Proof Society.

# Summer School: Day 2 and 3

We were glad to welcome Takako Nemoto, who joined us on the second day of the Summer School and gave her course on Reverse Mathematics.

As a treat, the participants of the Summer School had a trip to Rhossili and enjoyed a walk along the Welsh coastal path with stunning views. Big thanks to Arved Friedemann and Melissa Antonnelli for the beautiful photos.

# Proof Society Summer School

We are very glad to welcome all the participants of the 2nd International Summer School on Proof Theory.

The first day began with a lecture on **Universal Proof Theory** by Rosalie Iemhoff, followed by Wolfram Pohlers‘ talk on **Ordinal Analysis**, **Bounded Arithmetic** lecture from our own Arnold Beckmann, introduction to **Proof Mining** by Paulo Oliva, Paola Bruscoli’s talk on **Structural Proof Theory** and Anton Setzer’s lecture on **MLTT**.

We were lucky with both the lovely weather and the fact that Bay Campus is located right at the seafront, so the evening brought a nice treat for everyone in a form of a BBQ at the beach. Big thanks to Arnold, Faron for their grilling and Ulrich, Rosalie, Monika, Arved, Aled, Anton, Olga and everyone else who helped with the organisation.

# Erisa Karafili on forensic analysis of cyber-attacks

Today Erisa Karafili from the Imperial College London has given a talk on “Helping Forensic Analysts to Analyze and Attribute Cyber-Attacks” as a part of our Theory seminars.

**Abstract:** *The frequency and harmfulness of cyber-attacks are increasing every day, and with them also the amount of data that the cyber-forensics analysts need to collect and analyze. Analyzing and discovering who performed an attack or from where it originated would permit to put in act targeted mitigative and preventive measures. In my talk, I will present two techniques that help the forensics analyst to analyze and attribute cyber-attacks. The first technique is a formal analysis process that allows an analyst to filter the enormous amount of evidence collected and either identify crucial information about the attack (e.g., when it occurred, its culprit, its target) or, at the very least, perform a pre-analysis to reduce the complexity of the problem in order to then draw conclusions more swiftly and efficiently. The second technique is a novel argumentation-based reasoner (ABR) for analyzing and attributing cyber-attacks that includes in its reasoning technical and social evidence.*

# Logic Minisymposium at Swansea University

Tomorrow we are holding our end-of-summer logic minisymposium.

**Speakers:**

- Åsa Hirvonen
- Ken-etsu Fujita
- Masahiko Sato

**Schedule: **

2:00 Åsa Hirvonen (Helsinki University): On continuous logic

2:40 Coffee & Cake

3:00 Ken-etsu Fujita (Gunma University): A constructive proof of the Church—Rosser theorem

3:50 Masahiko Sato (Kyoto University): Unification of the Lambda-Calcululs and Combinatory Logic

On continuous logic, Åsa Hirvonen (Helsinki University)Continuous first order logic in its current form was developed at the beginning of this millennium to offer a language for the model theoretic study of metric structures, such as Banach spaces and probability spaces. It is a many-valued logic but has a different motivation and semantic than, e.g., Lukasiewicz logic. Many model theoretical properties of first order logic generalise to it, such as compactness and Löwenheim-Skolem theorems. This talk is a general introduction to the syntax and semantics as well as some basic properties of continuous logic.

A constructive proof of the Church—Rosser theorem, Ken-etsu Fujita (Gunma University)My motivation behind this talk comes from a quantitative analysis of reduction systems based on the two viewpoints, computational cost and computational orbit.

In the first part, we show that an upper bound function for the Church—Rosser theorem of type-free lambda-calculus with beta-reduction must be in the fourth level of the Grzegorczyk hierarchy. That is, the number of reduction steps to arrive at a common reduct is bounded by a function in the smallest Grzegorczyk class properly extending that of elementary functions. At this level we also find common reducts for the confluence property. The proof method developed here can be applied not only to type-free lambda-calculus with beta-eta-reduction

but also to typed lambda-calculi such as Pure Types Systems.In the second part, we propose a formal system of reduction paths for parallel reduction, wherein reduction paths are generated from a quiver by means of three path-operators, concatenation, monotonicity, and cofinality. Next, we introduce an equational theory and reduction rules for the reduction paths, and show that the rules on paths are terminating and confluent so that normal paths are obtained. Following the notion of normal paths, a graphical representation of reduction paths is provided, based on which unique path and universal common-reduct properties are established. Finally, transformation rules from a conversion sequence to a reduction path leading to the universal common-reduct are given, and path matrices are also defined as block matrices of adjacency matrices in order to count reduction orbits.

Unification of the Lambda-Calcululs and Combinatory Logic, Masahiko Sato (Kyoto University):The Lambda calculus and combinatory logic have been studied as two closely related but distinct systems of logic and computation. In this talk, however, we will argue that they are in fact one and the same calculus.

We substantiate our argument by introducing what we will call the external syntax and the internal syntax for the two calculi. The external syntax will be given as a natural common extension of syntax for the \lambda-calculus and combinatory logic.

The terms defined by the internal syntax will be characterized as the closed alpha eta normal terms of the external syntax. Thus, the external syntax provides us with human readable syntax containing all the traditional \lambda-terms and combinatory-terms, and the internal syntax is suitable for the infrastructure of a proof assistant.

This is an ongoing joint work with Takafumi Sakurai and Helmut Schwichtenberg.