Journals

On the generation of quantified lemmas
(with S. Hetzl, A. Leitsch, G. Reis, and D. Weller)
Journal of Automated Reasoning (2018)
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

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, Spinger

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

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.

Preprints

Fast cut-elimination using proof terms: an empirical study (2018)
pdf, slides

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