Publications

Journal articles

• Unifying splitting
  (with J. Blanchette and S. Tourret)
  Journal of Automated Reasoning 67(16) (2023)
  pdf, Springer
• 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

Conference and workshop proceedings

• 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
  pdf, OpenReview
• A unifying splitting framework
  (with J. Blanchette and S. Tourret)
  CADE 2021, A. Platzer and G. Sutcliffe (eds.), Springer LNCS 12699
  Springer
• Maintaining a library of formal mathematics
  CICM 2020, C. Benzmüller and B. Miller (eds.), Springer LNCS 12236
  pdf, slides, Springer, arXiv
• 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

• A unifying splitting framework
  Computational logic seminar at TU Wien, June 9, 2021
  slides
• 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, 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

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