Lukas Stevens

About me

Since October 2019, I am a doctoral candidate in Computer Science at the Chair for Logic and Verification supervised by Prof. Nipkow. My interests are automated theorem proving and the integration of automated methods into the theorem prover Isabelle. Currently, I am working on verifying proof-producing decision procedures for ground theories such as multi-level syllogistic (a fragment of set theory) and congruence closure.

Before starting as a doctoral candidate, I received my Bachelors and Masters in Computer Science at the Technical University of Munich. I was a tutor in Efficient Algorithms and Data Structures and a research assistant at the Chair for IT Security during my studies.

Conference Articles

• Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
  by Lukas Stevens
  Published in: Proceedings of CADE 2023, DOI: 10.1007/978-3-031-38499-8_28
  Preprint version available on arXiv
• A Verified Decision Procedure for Orders in Isabelle/HOL
  by Lukas Stevens and Tobias Nipkow
  Published in: Proceedings of ATVA 2021, DOI: 10.1007/978-3-030-88885-5_9
  Preprint version available on arXiv

Workshop Articles

• A Linter for Isabelle: Implementation and Evaluation
  by Yecine Megdiche, Fabian Huch and Lukas Stevens
  Appeared in the Isabelle Workshop 2022
  Preprint version available on arXiv
  

Entries in the Archive of Formal Proofs (AFP)

• MLSS Decision Procedure (Author)
• Order Extension and Szpilrajn’s Theorem (Contributor)

Teaching

• Winter 23/24: tutorial supervisor for Lambda Calculus
• Summer 23: tutorial supervisor for Theoretical Computer Science
• Winter 22/23: tutorial supervisor for Lambda Calculus
• Summer 22: tutorial (co-)supervisor for Grundlagen: Algorithmen und Datenstrukturen
• Winter 21/22: tutorial supervisor for Lambda Calculus
• Winter 20/21: (co-)organiser for the practical course Contributing to an Open Source Project
• Winter 20/21: tutorial (co-)supervisor for Functional Programming and Verification
• Summer 20: tutorial (co-)supervisor for Theoretical Computer Science
• Winter 19/20: tutorial (co-)supervisor for Functional Programming and Verification

Contact