
An extensible user interface for Lean 4
(with E. Ayers and W. Nawrocki)
ITP 2023

HyperTree proof search for neural theorem proving
(with G. Lample, T. Lacroix, M.A. Lachaux, A. Rodriguez, A. Hayat, T. Lavril, and X. Martinet)
NeurIPS 2022

A unifying splitting framework
(with J. Blanchette and S. Tourret)
CADE 2021, A. Platzer and G. Sutcliffe (eds.), Springer LNCS 12699

Maintaining a library of formal mathematics
CICM 2020, C. Benzmüller and B. Miller (eds.), Springer LNCS 12236

Herbrand constructivization for automated
intuitionistic theorem proving
TABLEAUX 2019, S. Cerrito and A. Popescu (eds.), Springer LNCS 11714

Complexity of decision problems on
totally rigid acyclic tree grammars
(with S. Eberhard and S. Hetzl)
DLT 2018, Hoshi M. and Seki S. (eds.), Springer LNCS 11088

Fast cutelimination using proof terms:
an empirical study
CL&C 2018, S. Berardi and A. Miquel (eds.), EPTCS 281

Efficient translation of sequent calculus proofs
into natural deduction proofs
(with M. Schlaipfer)
PAAR 2018, B. Konev, J. Urban, and P. Rümmer (eds.), CEURWS 2162

A metaprogramming framework for formal verification
(with S. Ullrich, J. Roesch, J. Avigad, and L. de Moura)
ICFP 2017, Proceedings of the ACM on Programming Languages 1(ICFP) (2017)

System description: GAPT 2.0
(with S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, and S. Zivota)
IJCAR 2016, N. Olivetti and A. Tiwari (eds.), Springer LNCS 9706

A unifying splitting framework
Computational logic seminar at TU Wien, June 9, 2021

Integration of generalpurpose automated theorem provers in Lean

Computational complexity of grammars for proofs with induction

Herbrand constructivization for automated intuitionistic theorem proving

Tree grammars for induction on inductive data types modulo equational
theories

Dependently typed superposition in Lean

Extracting expansion trees from
resolution proofs with splitting and definitions
Theory & Logic seminar at TU Wien, January 17, 2018

The Lean Theorem Prover

Complexity of decision problems on TRATGs

(with L. de Moura, J. Roesch, and S. Ullrich)
POPL 2017, January 16, 2017

Minimal grammars via MaxSAT
Theory & Logic seminar at TU Wien, April 13, 2016

Finding loop invariants using tree grammars
Theory & Logic seminar at TU Wien, January 28, 2015