Program

All timestamps are in CEST (UTC+02:00). The current local time is .

#I0		Class A (Zaal 1.05)

9:30		Registration


10:00		Impredicative ordinal analysis Henry Towsner Tutorial





11:00		Coffee break


11:30		Tarski-style axiomatic truth theories Ali Enayat Tutorial





12:30		Lunch











14:30		Impredicative ordinal analysis Henry Towsner Tutorial





15:30		Coffee break


16:00		Tarski-style axiomatic truth theories Ali Enayat Tutorial





17:00

#I0		Class A (Zaal 1.05)

10:00		Impredicative ordinal analysis Henry Towsner Tutorial





11:00		Coffee break


11:30		Tarski-style axiomatic truth theories Ali Enayat Tutorial





12:30		Lunch











14:30		The ubiquitous interpretation Albert Visser Tutorial





15:30		Coffee break


16:00		Introduction to bounded arithmetic Raheleh Jalali Tutorial





17:00

#I0		Class A (Zaal 1.05)

10:00		The ubiquitous interpretation Albert Visser Tutorial





11:00		Coffee break


11:30		Introduction to bounded arithmetic Raheleh Jalali Tutorial





12:30		Lunch











14:30		The ubiquitous interpretation Albert Visser Tutorial





15:30		Coffee break


16:00		Introduction to bounded arithmetic Raheleh Jalali Tutorial





17:00
17:10		Social excursion








18:40

#I0		Class A (Zaal 1.05)		Class B (Zaal 1.07)

9:00	Registration


9:30	Taming proof systems towards uniform interpolation Iris van der Giessen Invited




10:20	Coffee break


10:50	A modular ordinal analysis for fragments of induction principles Koshiro Ichikawa Contributed	On the non-classical, non-monotonic and uniform proof-theoretic validity of Weak Excluded Middle Antonio Piccolomini d'Aragona Contributed

11:10	A classification of the provably total set-recursive functions of KPl, KPl^r and W-KPl Anton Fernández Contributed	A survey of two strands in proof-theoretic semantics Leonardo Ceragioli, Francesco Montesi, Antonio Piccolomini d'Aragona Contributed

11:30	Predicative recursion on the Veblen hierarchy Vitor Greati Contributed	Meaningful proof systems and bilateralism Robin Martinot Contributed

11:50	Rewrite normalization in tree rewriting calculi for strictly positive logics Sofía Santiago-Fernández, David Fernández-Duque, Joost Joosten Contributed	Unification for weak classical modal logics Mojtaba Mojtahedi Contributed

12:10	The barrier Ramsey theorem Andrea Volpi Contributed
	The barrier Ramsey theorem Andrea Volpi Contributed
12:30	Lunch








14:00	Justification logic for intuitionistic modal logic Paaras Padhiar Contributed	Predicative set theory: a new foundation for feasible mathematics Amirhossein Akbar Tabatabai Contributed

14:20	Interpolation for the two-way modal $µ$ -calculus Johannes Kloibhofer Contributed	Towards computing uniform interpolants for KM in Rocq Ian Shillito Contributed

14:40	The modal cube revisited: semantics without worlds Elaine Pimentel Contributed	Non-deterministic operations in applicative theories Marcel Ertel Contributed

15:00	Three alternative systems with alternatives Luiz Carlos Pereira Contributed	Proof logging the generalized totalizer encoding Carlos Cantero Contributed

15:20	Coffee break


15:50	Proof theory of stable ordinals Toshiyasu Arai Invited




16:40
16:50	Proof Society general assembly





17:50









19:30	Workshop dinner














22:00

#I0		Class A (Zaal 1.05)

9:30		The norms of RCA₀ Juan Pablo Aguilera Invited




10:20		Coffee break


10:50		Correctness of the AKS primality algorithm in bounded arithmetic Raheleh Jalali Contributed

11:10		Speedup for Presburger arithmetic and real closed fields Julien Daoud Contributed

11:30		Definiteness properties of arithmetical theories Piotr Gruza Contributed

11:50		General inductive definitions and their proof theory from a perspective of knowledge representation Robbe Van den Eede Contributed

12:10		Bilateralist base-extension semantics with incompatible proofs and refutations Victor Barroso Nascimiento, Maria Osório Costa, Elaine Pimentel Contributed

12:30		Lunch








14:00		A non-wellfounded and labelled sequent calculus for bimodal provability logic Justus Becker Contributed

14:20		Non-wellfounded languages and proofs Philipp Provenzano Contributed

14:40		Extracting computational content from cyclic proofs using higher order recursion schemes Giacomo Barlucchi Contributed

15:00		Matching (co)patterns with cyclic proofs Lide Grotenhuis Contributed

15:20		Coffee break


15:50		In memory of Wolfram Pohlers - a personal account Arnold Beckmann Invited




16:40
16:50		Predicative foundations of the Mahlo universe in Martin-Löf type theory Anton Setzer Invited




17:40		Best Student Presentation award ceremony
		Best Student Presentation award ceremony
18:00