# Publications

## Journals

*On the generation of quantified lemmas*

(with S. Hetzl, A. Leitsch, G. Reis, and D. Weller)

Journal of Automated Reasoning 63(1) (2019)

pdf,
Springer

*Algorithmic compression of finite tree languages by rigid acyclic grammars*

(with S. Eberhard and S. Hetzl)

ACM Transactions on Computational Logic 18(4) (2017)

pdf,
ACM

## Proceedings

*Herbrand constructivization for automated
intuitionistic theorem proving*

TABLEAUX 2019, S. Cerrito and A. Popescu (eds.), Springer LNCS 11714

pdf,
slides,
Springer

*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

pdf,
slides,
Springer

*Fast cut-elimination using proof terms:
an empirical study*

CL&C 2018, S. Berardi and A. Miquel (eds.), EPTCS 281

pdf, slides,
EPTCS, arXiv

*Efficient translation of sequent calculus proofs
into natural deduction proofs*

(with M. Schlaipfer)

PAAR 2018, B. Konev, J. Urban, and P. Rümmer (eds.), CEUR-WS 2162

pdf, slides,
CEUR

*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)

pdf,
ACM

*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

pdf,
slides,
Springer

## Other talks

*Integration of general-purpose automated theorem provers in Lean*

FoMM 2020, January 6-10 2020,
slides.

*Computational complexity of grammars for proofs with induction*

PTADADPT 2019, October 23-25 2019,
slides.

*Herbrand constructivization for automated intuitionistic theorem proving*

FISP 2018, December 7-8 2018,
slides.

*Tree grammars for induction on inductive data types modulo equational
theories*

WAIT 2018,
June 28, 2018,
slides.

*Dependently typed superposition in Lean*

Matryoshka 2018,
June 27, 2018,
slides, code.

*Extracting expansion trees from
resolution proofs with splitting and definitions*

Theory & Logic seminar at TU Wien,
January 17, 2018,
slides.

*The Lean Theorem Prover*

Alpine Verification Meeting 2017,
September 18, 2017,
slides,
materials.

*Complexity of decision problems on TRATGs*

Herbrand’s Theorem Revisited (workshop),
May 5, 2017,
slides.

*The Lean Theorem Prover*

(with L. de Moura, J. Roesch, and S. Ullrich)

POPL 2017, January 16, 2017,
slides,
materials.

*Minimal grammars via MaxSAT*

Theory & Logic seminar at TU Wien,
April 13, 2016,
slides.

*Finding loop invariants using tree grammars*

Theory & Logic seminar at TU Wien,
January 28, 2015,
slides.

## Drafts

*Induction formulas and term structure* (2019)

pdf

*Extracting expansion trees from resolution
proofs with splitting and definitions* (2018)

pdf

*Tree grammars for induction on inductive data
types modulo equational theories* (2018)

(with S. Hetzl)

pdf