FroCoS/ITP/TABLEAUX '25

Recordings, Slides, and Links


Main page
FroCoS 2025 - ITP 2025 - TABLEAUX 2025
Rocq 2025 - Lean 2025
Programme booklet, Programme on 2 pages

Jump to:

Rocqshop

 - Rocq 1 - Rocq 2 - Rocq 3 - Rocq 4

ITP

 - ITP 1 - ITP 2 - ITP 3 - ITP 4- ITP 5- ITP 6- ITP 7- ITP 8- ITP 9- ITP 10- ITP 12- ITP 13- ITP 14- ITP 15

TABLEAUX

 - TABLEAUX 1 - TABLEAUX 2 - TABLEAUX 3 - TABLEAUX 4 - TABLEAUX 5 - TABLEAUX 6 - TABLEAUX 7 - TABLEAUX 8 - TABLEAUX 9
TABLEAUX/FroCoS joint invited speaker

FroCoS

 - FroCoS 1 - FroCoS 2 - FroCoS 3 - FroCoS 4 - FroCoS 5 - FroCoS 6 - FroCoS 7 - FroCoS 8

Lean Workshop

 - Lean 1 - Lean 2 - Lean 4
YouTube playlists:

All

 -

Rocqshop

 -

ITP

 -

TABLEAUX

 -

FroCoS

 -

Lean

Rocqshop (27 September)

Rocqshop session 1 (27 September 2025)

Rocqshop session 2 (27 September 2025)

Rocqshop session 3 (27 September 2025)

  • Automating Alignments of HOL Light Inductive Types and Recursive Functions in Rocq

    [Recording] [Slides] 
    • Author/Speaker: Antoine Gontard

  • Certified Programming with Dependent Types Made Simple with Proxy-Based Small Inversions

    [Recording] [Slides] 
    • Speaker: Basile Gros
    • Authors: Pierre Corbineau, Basile Gros, Jean-François Monin

  • Extending Sort Polymorphism with Elimination Constraints in Rocq

    [Recording] [Slides] 
    • Speaker: Johann Rosain
    • Authors: Tomás Díaz, Kenji Maillard, Johann Rosain, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter

Rocqshop session 4 (27 September 2025)

  • LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback

    [Recording] [Slides] 
    • Speaker: Théo Stoskopf
    • Authors: Théo Stoskopf, Jules Viennot, Cyril Cohen

  • Can States Be Decidable in Inquisitive Mechanizations?

    [Recording] [Slides] 
    • Speaker: Tadeusz Litak
    • Authors: Max Ole Elliger, Tadeusz Litak

  • MiniF2F in Rocq: Automatic Translation Between Proof Assistants: A Case Study

    [Recording] [Slides] 
    • Speaker: Jules Viennot
    • Authors: Jules Viennot, Guillaume Baudart, Emilio Jesus Gallego Arias, Marc Lelarge

  • HotdocX & jsCoq: A Platform for Interactive, AI-Augmented and Monetizable Coq Experiences

    [Recording] [Slides] 
    • Author/Speaker: Christopher Mary

ITP (28 September — 1 October)

ITP session 1 (28 September 2025)

  • Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

    [DOI] [Recording] [Slides] 
    • Speaker: Hanna Lachnitt
    • Authors: Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Andrew Reynolds, Jibiana Jakpor, Bruno Andreotti, Clark Barrett, Hans-Jörg Schurr, Cesare Tinelli

  • Formalizing Splitting in Isabelle/HOL

    [DOI] [Slides] 
    • Speaker: Sophie Tourret
    • Authors: Ghilain Bergeron, Florent Krasnopol, Sophie Tourret

  • Sledgehammering without ATPs

    [DOI] [Recording] [Slides] 
    • Speaker: Martin Desharnais
    • Authors: Martin Desharnais, Jasmin Blanchette

ITP session 2 (28 September 2025)

  • Taming Floating-Point Rounding Errors with Proofs

    [DOI] [Recording] [Slides] 
    • Author/Speaker: Laura Titolo

  • Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic

    [DOI] [Recording] [Slides] 
    • Speaker: Robert Krebbers
    • Authors: Robert Krebbers, Luko van der Maas, Enrico Tassi

ITP session 3 (28 September 2025)

  • Formalising Subject Reduction and Progress for Multiparty Session Processes

    [DOI] [Recording] [Slides] 
    • Speaker: Tadayoshi Kamegai, Nobuko Yoshida
    • Authors: Burak Ekici, Tadayoshi Kamegai, Nobuko Yoshida

  • Certified Implementability of Global Multiparty Protocols

    [DOI] [Recording] [Slides] 
    • Speaker: Elaine Li
    • Authors: Elaine Li, Thomas Wies

  • GOL in GOL in HOL: Verified Circuits in Conway's Game of Life

    [DOI] [Recording] [Slides] 
    • Speaker: Magnus Myreen
    • Authors: Magnus Myreen, Mario Carneiro

  • Nondeterministic Asynchronous Dataflow in Isabelle/HOL

    [DOI] [Recording] [Slides] 
    • Speaker: Rafael Castro G. Silva
    • Authors: Rafael Castro G. Silva, Laouen Fernet, Dmitriy Traytel

ITP session 4 (29 September 2025)

  • An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems

    [DOI] [Recording] [Slides] 
    • Author/Speaker: Dohan Kim

  • Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation

    [DOI] [Recording] [Slides] 
    • Speaker: Alessandro Bruni
    • Authors: Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa

  • Towards Automating Permutation Proofs in Coq: A Reflexive Approach with Iterative Deepening Search

    [DOI] [Slides] 
    • Author/Speaker: Nadeem Abdul Hamid

ITP session 5 (29 September 2025)

  • Nanopass Back-Translation of Call- Return Trees for Mechanized Secure Compilation Proofs

    [DOI] [Recording] [Slides] 
    • Speaker: Jérémy Thibault
    • Authors: Jérémy Thibault, Joseph Lenormand, Cătălin Hrițcu

  • Formalizing the Hidden Number Problem in Isabelle/HOL

    [DOI] [Recording] [Slides] 
    • Speaker: Sage Binder
    • Authors: Sage Binder, Eric Ren, Katherine Kosaian

  • On Verifying Secret Control Flow Elimination

    [DOI] [Recording] [Slides] 
    • Speaker: David Knothe
    • Authors: David Knothe, Oliver Bringmann

ITP session 6 (29 September 2025)

  • A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

    [DOI] [Recording] [Slides] 
    • Author/Speaker: Joshua M. Cohen

  • Program Optimisations via Hylomorphisms for Extraction of Executable Code

    [DOI] [Recording] [Slides] 
    • Speaker: David Castro Perez
    • Authors: David Castro Perez, Marco Paviotti, Michael Vollmer

ITP session 7 (29 September 2025)

  • Mechanising Böhm Trees and λη-Completeness

    [DOI] [Recording] [Slides] 
    • Speaker: Michael Norrish
    • Authors: Chun Tian, Michael Norrish

  • Barendregt's Theory of the Lambda-Calculus, Refreshed and Formalized

    [DOI] [Recording] [Slides] 
    • Speaker: Adrienne Lancelot
    • Authors: Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs

  • A Verified Cost Model for Call-by-Push-Value

    [DOI] [Recording] [Slides] 
    • Speaker: Zhuo Chen
    • Authors: Zhuo Chen, Johannes Åman Pohjola, Christine Rizkallah

ITP session 8 (30 September 2025)

  • Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant

    [DOI] [Recording] 
    • Author/Speaker: Kathrin Stark

  • Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

    [DOI] [Recording] [Slides] 
    • Speaker: Jan van Brügge
    • Authors: Jan van Brügge, Andrei Popescu, Dmitriy Traytel

ITP session 9 (30 September 2025)

  • Formally Verifying a Vertical Cell Decomposition Algorithm

    [DOI] [Recording] [Slides] 
    • Speaker: Yves Bertot
    • Authors: Yves Bertot, Thomas Portet

  • Verification of the CVM Algorithm with a Functional Probabilistic Invariant

    [DOI] [Recording] 
    • Speaker: Emin Karayel
    • Authors: Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan

  • Verifying an Efficient Algorithm for Computing Bernoulli Numbers

    [DOI] [Recording] [Slides] 
    • Speaker: Manuel Eberl
    • Authors: Manuel Eberl, Peter Lammich

ITP session 10 (30 September 2025)

  • Automatically Generalizing Proofs and Statements

    [DOI] [Recording] [Slides] 
    • Speaker: Anshula Gandhi
    • Authors: Anshula Gandhi, Anand Rao Tadipatri, Timothy Gowers

  • Canonical for Automated Theorem Proving in Lean

    [DOI] [Recording] [Slides] 
    • Speaker: Chase Norman
    • Authors: Chase Norman, Jeremy Avigad

  • Verifying Datalog Reasoning with Lean

    [DOI] [Recording] [Slides] 
    • Speaker: Johannes Tantow
    • Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch

ITP session 12 (1 October 2025)

  • Algebra is Half the Battle: Verifying Presentations for Graded Unipotent Chevalley Groups

    [DOI] [Recording] [Slides] 
    • Speaker: Cayden Codel
    • Authors: Eric Wang, Arohee Bhoja, Cayden Codel, Noah G. Singer

  • Formalising New Mathematics in Isabelle: Diagonal Ramsey

    [DOI] [Recording] [Slides] 
    • Author/Speaker: Lawrence Paulson

  • A Natural Language Formalization of Perfectoid Rings in Naproche

    [DOI] [Recording] [Slides] 
    • Author/Speaker: Peter Koepke

ITP session 13 (1 October 2025)

  • A Formalization of Divided Powers in Lean

    [DOI] [Recording] [Slides] 
    • Speaker: Maria Inés de Frutos-Fernández
    • Authors: Antoine Chambert-Loir, Maria Inés de Frutos-Fernández

  • A Formal Proof of Complexity Bounds on Diophantine Equations

    [DOI] [Recording] [Slides] 
    • Author/Speaker: Jonas Bayer, Marco David

  • A Formal Analysis of Algorithms for Matroids and Greedoids

    [DOI] [Slides] 
    • Speaker: Thomas Ammer
    • Authors: Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa

ITP session 14 (1 October 2025)

  • Scott’s Representation Theorem and the Univalent Karoubi Envelope

    [DOI] [Recording] [Slides] 
    • Speaker: Benedikt Ahrens
    • Authors: Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens

  • Formalising Inductive and Coinductive Containers

    [DOI] [Recording] [Slides] 
    • Speaker: Stefania Damato
    • Authors: Stefania Damato, Thorsten Altenkirch, Axel Ljungström

  • Formalizing colimits in Cat

    [DOI] [Recording] [Slides] 
    • Speaker: Mario Carneiro
    • Authors: Mario Carneiro, Emily Riehl

ITP session 15 (1 October 2025)

  • Abstract, Compositional Consistency: Isabelle/ HOL Locales for Completeness à la Fitting

    [DOI] [Recording] [Slides] 
    • Speaker: Anders Schlichtkrull
    • Authors: Asta Halkjær From, Anders Schlichtkrull

  • Finiteness of Symbolic Derivatives in Lean

    [DOI] [Recording] [Slides] 
    • Speaker: Ekaterina Zhuchko
    • Authors: Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, G. Ebner

  • A Certified Proof Checker for Deep Neural Network Verification in Imandra

    [DOI] [Recording] [Slides] 
    • Speaker: Omri Isac
    • Authors: Remi Desmartin, Omri Isac, Ekaterina Komendantskaya, Kathrin Stark, Grant Passmore, Guy Katz

  • LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean

    [DOI] [Recording] [Slides] 
    • Speaker: Eric Vin
    • Authors: Eric Vin, Kyle Miller, Daniel J. Fremont

TABLEAUX (27 September — 29 September)

TABLEAUX session 1 (27 September 2025)

  • A Tableau System for First-Order Logic with Standard Names

    [DOI] [Recording] [Slides] 
    • Speaker: Jens Claßen
    • Authors: Jens Claßen, Torben Braüner

  • Bounded Inquisitive Logics: Sequent Calculi and Schematic Validity

    [DOI] [Recording] [Slides] 
    • Speaker: Tadeusz Litak
    • Authors: Tadeusz Litak, Katsuhiko Sano

  • Analytic Calculi for Logics of Indicative Conditionals

    [DOI] [Recording] [Slides] 
    • Speaker: Vitor Rodrigues Greati
    • Authors: Vitor Rodrigues Greati, Sérgio Marcelino, Miguel Muñoz Pérez, Umberto Rivieccio

TABLEAUX session 2 (27 September 2025)

  • Analytic Proofs for Tense Logic

    [DOI] [Slides] 
    • Speaker: Revantha Ramanayake
    • Authors: Agata Ciabattoni, Timo Lang, Revantha Ramanayake

  • Improved Decision Procedures for Multimodal Tense Logic Using CEGAR-Tableaux

    [DOI] [Recording] [Slides] 
    • Speaker: Rajeev Goré
    • Authors: Rajeev Goré, Cormac Kikkert

  • Interpolation for Converse PDL

    [DOI] [Recording] [Slides] 
    • Speaker: Francisco Carlos Trucco Dalmas
    • Authors: Johannes Kloibhofer, Francisco Carlos Trucco Dalmas, Yde Venema

TABLEAUX session 3 (27 September 2025)

  • Semi-competitive Differential Game Logic

    [DOI] [Recording] [Slides] 
    • Speaker: Julia Butte
    • Authors: Julia Butte, André Platzer

  • Base-Extension Semantics for Intuitionistic Modal Logics

    [DOI] [Recording] [Slides] 
    • Speaker: Yll Buzoku
    • Authors: Yll Buzoku, David Pym

  • Forward Proof Search for Intuitionistic Multimodal K Logics

    [DOI] [Recording] [Slides] 
    • Author/Speaker: Niels Voorneveld

TABLEAUX session 4 (27 September 2025)

  • A Proof-Theoretic View of Basic Intuitionistic Conditional Logic

    [DOI] [Recording] [Slides] 
    • Speaker: Tiziano Dalmonte
    • Authors: Tiziano Dalmonte, Marianna Girlando

  • Intuitionistic μ-Calculus with the Lewis Arrow

    [DOI] [Recording] [Slides] 
    • Speaker: Lide Grotenhuis
    • Authors: Lide Grotenhuis, Bahareh Afshari

  • Justification Logic for Intuitionistic Modal Logic

    [DOI] [Recording] [Slides] 
    • Speaker: Paaras Padhiar
    • Authors: Sonia Marin, Paaras Padhiar

TABLEAUX session 5 (28 September 2025)

  • Skolemization Beyond Intuitionistic Logic: The Role of Quantifier Shifts

    [Recording] [Slides] 
    • Author/Speaker: Raheleh Jalali

  • A Sequent Calculus Perspective on Base-Extension Semantics

    [DOI] [Recording] [Slides] 
    • Speaker: Victor Barroso-Nascimento
    • Authors: Victor Barroso-Nascimento, Ekaterina Piotrovskaya, Elaine Pimentel

TABLEAUX session 6 (28 September 2025)

  • Designing a Safe Forward Chaining Tactic Using Productive Proofs

    [DOI] [Slides] 
    • Speaker: Arunava Gantait
    • Authors: Kaustuv Chaudhuri, Arunava Gantait, Dale Miller

  • Intuitionistic BV

    [DOI] 
    • Speaker: Matteo Acclavio
    • Authors: Matteo Acclavio, Lutz Straßburger

  • An Agda Formalization of Nonassociative Lambek Calculus and Its Metatheory

    [DOI] [Recording] [Slides] 
    • Speaker: Cheng-Syuan Wan
    • Authors: Niccolò Veltri, Cheng-Syuan Wan

TABLEAUX session 7 (28 September 2025)

  • Cyclic System for an Algebraic Theory of Alternating Parity Automata

    [DOI] [Recording] [Slides] 
    • Speaker: Anupam Das
    • Authors: Anupam Das, Abhishek De

  • A Sequent Calculus for Trace Formula Implication

    [DOI] [Recording] [Slides] 
    • Speaker: Niklas Heidler
    • Authors: Niklas Heidler, Reiner Hähnle

  • On Solving String Equations via Powers and Parikh Images

    [DOI] [Recording] [Slides] 
    • Speaker: Clemens Eisenhofer
    • Authors: Clemens Eisenhofer, Theodor Seiser, Laura Kovács, Nikolaj Bjørner

TABLEAUX session 8 (29 September 2025)

  • A Gödel Modal Logic over Witnessed Crisp Models

    [DOI] [Recording] [Slides] 
    • Speaker: Mauro Ferrari
    • Authors: Mauro Ferrari, Camillo Fiorentini, Ricardo Oscar Rodriguez

  • The Modal Cube Revisited: Semantics without Worlds

    [DOI] [Recording] [Slides] 
    • Speaker: Carlos Olarte
    • Authors: Renato Leme, Carlos Olarte, Elaine Pimentel, Marcelo Esteban Coniglio

  • Refined Tableau Systems for Some Modal Logics of Confluence

    [DOI] [Recording] [Slides] 
    • Speaker: Kiana Samadpour Motalebi
    • Authors: Kiana Samadpour Motalebi, Renate A. Schmidt, Cláudia Nalon

TABLEAUX session 9 (29 September 2025)

  • Non-Wellfounded Proof Theory for Interpretability Logic

    [DOI] [Recording] [Slides] 
    • Speaker: Borja Sierra Miranda
    • Authors: Borja Sierra Miranda, Sebastijan Horvat, Thomas Studer

  • Finding Connections via Satisfiability Solving

    [DOI] [Recording] [Slides] 
    • Speaker: Clemens Eisenhofer
    • Authors: Clemens Eisenhofer, Michael Rawson, Laura Kovács

  • Constraint learning for non-confluent proof search

    [DOI] [Recording] [Slides] 
    • Speaker: Clemens Eisenhofer
    • Authors: Michael Rawson, Clemens Eisenhofer, Laura Kovács

TABLEAUX/FroCoS joint invited speaker (29 September 2025)

  • Towards a Universal Interactive Theorem Proving Interface

    [Recording] [Slides] 
    • Author/Speaker: Kaustuv Chaudhuri

FroCoS (29 September — 1 October)

FroCoS session 1 (29 September 2025)

  • The Expressive Power of Description Logics with Numerical Constraints over Restricted Classes of Models

    [DOI] [Recording] [Slides] 
    • Speaker: Filippo De Bortoli
    • Authors: Franz Baader, Filippo De Bortoli

  • Reasoning in OWL 2 EL with Hierarchical Concrete Domains

    [DOI] [Slides] 
    • Author/Speaker: Francesco Kriegel

  • The Concrete Evonne: Visualization Meets Concrete Domain Reasoning

    [DOI] [Recording] [Slides] 
    • Speaker: Christian Alrabbaa
    • Authors: Christian Alrabbaa, Franz Baader, Raimund Dachselt, Alisa Kovtunova, Julián Méndez

FroCoS session 2 (30 September 2025)

  • The Dependently Typed Higher-Order Form for the TPTP World

    [DOI] [Recording] [Slides] 
    • Speaker: Daniel Ranalter
    • Authors: Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe

  • An Analytic Representation of the Semantics of First-Order S5

    [DOI] [Recording] [Slides] 
    • Speaker: Mariami Gamsakhurdia
    • Authors: Anela Lolic, Matthias Baaz, Mariami Gamsakhurdia

  • Deciding Satisfiability for Overlaid Symbolic Heaps

    [DOI] [Recording] [Slides] 
    • Speaker: Quentin Petitjean
    • Authors: Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu

FroCoS session 3 (30 September 2025)

  • Weighted Rewriting

    [DOI] [Recording] [Slides] 
    • Speaker: Martin Avanzini
    • Authors: Martin Avanzini, Akihisa Yamada

  • Data-Driven Runtime Complexity Analysis

    [DOI] [Recording] [Slides] 
    • Speaker: Samuel Frontull
    • Authors: Samuel Frontull, Manuel Meitinger, Georg Moser

  • Graph Embedded Rewrite Systems: Combination and Undecidability Results

    [DOI] [Recording] [Slides] 
    • Speaker: Christophe Ringeissen
    • Authors: Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen

FroCoS session 4 (30 September 2025)

  • Automatic Static Program Analysis via Constrained Term Rewriting

    [Recording] [Slides] 
    • Author/Speaker: Carsten Fuhs

  • Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems

    [DOI] [Recording] [Slides] 
    • Speaker: Naoki Nishida
    • Authors: Naoki Nishida, Misaki Kojima, Yuto Nakamura

FroCoS session 5 (30 September 2025)

  • Iterative Monomorphisation

    [DOI] [Slides] 
    • Speaker: Tanguy Bozec
    • Authors: Tanguy Bozec, Jasmin Blanchette

  • Subtyping in Dependently-Typed Higher-Order Logic

    [DOI] [Slides] 
    • Speaker: Colin Rothgang
    • Authors: Colin Rothgang, Florian Rabe

  • Context-Aware Clause Selection Using Symbol Name Meanings in Theorem Proving

    [DOI] [Slides] 
    • Author/Speaker: Claudia Schon

FroCoS session 6 (1 October 2025)

  • When GNNs Met a Word Equations Solver: Learning to Rank Equations

    [DOI] [Recording] [Slides] 
    • Speaker: Julie Cailler
    • Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer

  • A Finite Abstraction of Real-Valued Functions for Complete Reasoning about Influence

    [DOI] [Recording] [Slides] 
    • Speaker: Sören Möller
    • Authors: Sören Möller, Florian Bruse, Martin Lange

  • Number Theory Combination: Natural Density and SMT

    [DOI] [Recording] [Slides] 
    • Speaker: Guilherme Toledo
    • Authors: Guilherme Toledo, Yoni Zohar

FroCoS session 7 (1 October 2025)

  • Polite Combination in Parametric Array Theories

    [DOI] [Recording] [Slides] 
    • Speaker: Rodrigo Raya
    • Authors: Rodrigo Raya, Christophe Ringeissen

  • Shininess, Strong Politeness, and Unicorns

    [DOI] [Recording] [Slides] 
    • Speaker: Benjamin Przybocki
    • Authors: Benjamin Przybocki, Guilherme Toledo, Yoni Zohar

  • Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories

    [DOI] [Recording] [Slides] 
    • Speaker: Gabriele Masina
    • Authors: Gabriele Masina, Roberto Sebastiani

FroCoS session 8 (1 October 2025)

  • Checking Linear Integer Arithmetic Proofs in Lambdapi

    [DOI] [Recording] [Slides] 
    • Speaker: Alessio Coltellacci
    • Authors: Alessio Coltellacci, Stephan Merz

  • Certifying rlive: A New Proof Strategy for Liveness Model Checking

    [DOI] [Recording] [Slides] 
    • Speaker: Giulia Sindoni
    • Authors: Alberto Griggio, Giulia Sindoni, Stefano Tonetta

Lean Workshop (2 October)

Lean Workshop session 1 (2 October 2025)

Lean Workshop session 2 (2 October 2025)

  • Automatic Geometry Theorem Proving Using Polynomial Elaboration

    [Recording] [Slides] [Abstract] 
    • Author/Speaker: Mauricio Barba da Costa

  • The Formal Conjectures Repo

    [Recording] [Slides] [Abstract] 
    • Author/Speaker: Moritz Firsching

  • Formalizing Possibly Infinite Trees of Finite Degree

    [Recording] [Slides] [Abstract] 
    • Author/Speaker: Lukas Gerlach

  • Verifying a Real-World Regex Implementation

    [Recording] [Slides] [Abstract] 
    • Author/Speaker: Yulu Pan

Lean Workshop session 4 (2 October 2025)