A picture of me

Hello! The picture of me on the right ☛ is increasingly inaccurate but it will have to do.

I am a researcher in the functional programming group of the Computer Science and Engineering department at Chalmers University of Technology. These days I mostly work on automated reasoning; in earlier times I did a lot of property-based testing. I wrote the equational theorem prover Twee and co-wrote the automated conjecturing tool QuickSpec.

Finding me

Draft publications

  • Writing a fast theorem prover in Haskell, incomplete draft. Presented at IFL 2026. [pdf].

  • Readable proofs for the Horn fragment, with Lydia Kondylidou, Jasmin Blanchette, Uwe Waldmann. [pdf].

  • Lemmanaid: Neuro-symbolic lemma conjecturing, with Yousef Alhessi, Sólrun Halla Einarsdóttir, George Granberry, Emily First, Moa Johansson, Sorin Lerner. [arxiv].

Publications

  • Twitch: Learning Abstractions for Equational Theorem Proving, with Guy Axelrod, Moa Johansson. IJCAR 2026. [arxiv].

  • Multilingual Autoformalization via Fine-tuning Large Language Models with Symbolically Generated Data, with Pei Huang, Aarne Ranta. SCML. [doi | pdf].

  • Karp: Språkbanken’s data editing platform, with Lars Borin, Emma Sköldberg, Ann Lillieström, Maria Öhrman, Jonatan Uppström, Louise Holmer. Chapter in book "Sixty years of Swedish computational lexicography". [doi].

  • Binary indexes for optimising corpus queries, with Peter Ljunglöf, Mijo Thoresson, Viktor Salomonsson. KONVENS 2024. [acl].

  • Lemma discovery and strategies for automated induction, with Sólrún Halla Einarsdóttir, Marton Hajdu, Moa Johansson, Martin Suda. IJCAR 2024. [pdf].

  • QuickerCheck: Implementing and evaluating a parallel run-time for QuickCheck, with Robert Krook, Bo Joel Svensson, Koen Claessen. IFL 2023. [arxiv].

  • Exploring Mathematical Conjecturing with Large Language Models, with Moa Johansson. NeSy 2023. [pdf].

  • Testing cyber-physical systems with a line-search falsification method, with Zahra Ramezani, Koen Claessen, Martin Fabian, Knut Åkesson. IEEE TCAD. [pdf].

  • Conjectures, Tests and Proofs: An overview of theory exploration, with Moa Johansson. VPT 2021. [pdf | arxiv].

  • Twee: An Equational Theorem Prover (System Description). CADE 2021. [pdf].

  • Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing with Sólrún Halla Einarsdóttir, Moa Johansson. IFL 2020. [pdf].

  • Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans with Johan Eddeland, Koen Claessen, Zahra Ramezani, Sajed Miremadi, Knut Åkesson. IEEE TCAD. [arxiv].

  • Testing Safety PLCs using QuickCheck with David Thönnessen, Martian Fabian, Koen Claessen, Stefan Kowalewski. IEEE CASE 2019. [pdf].

  • Safety at Speed: in-place array algorithms from pure functional programs by safely reusing storage with Markus Aronsson, Koen Claessen, Mary Sheeran. FHPNC 2019. [pdf].

  • Evaluating Two Semantics for Falsification using an Autonomous Driving Example with Zahra Ramezani, Martin Fabian, Knut Åkesson. INDIN 2019. [pdf].

  • Inferring morphological rules from small examples using 0/1 linear programming with Ann Lillieström, Koen Claessen. NoDaLiDa 2019. [pdf].

  • Understanding formal specifications through good examples with Alex Gerdes, John Hughes, Stefan Hanenberg, Sebastian Ivarsson, Meng Wang. Erlang Workshop 2018. [pdf].

  • Efficient encodings of first-order Horn formulas in equational logic with Koen Claessen. IJCAR 2018. [pdf].

  • Using valued Booleans to find simpler counterexamples in random testing of cyber-physical systems with Koen Claessen, Johan Eddeland, Zahra Ramezani and Knut Åkesson. Workshop on Discrete Event Systems. [pdf].

  • Quick specifications for the busy programmer with Moa Johansson, Koen Claessen, Maximilian Algehed. Journal of functional programming. [pdf | jfp | website].

  • Encoding monomorphic and polymorphic types, with Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu. Logical Methods in Computer Science. [pdf | lmcs].

  • Find more bugs with QuickCheck! with John Hughes, Ulf Norell, Thomas Arts. Automation of Software Test 2016. [pdf | acm].

  • TIP: tools for inductive provers with Dan Rosén. LPAR 2015. [pdf | springer | website].

  • Linking Unit Tests and Properties with Alex Gerdes, John Hughes, Thomas Arts. Erlang workshop 2015. [paper | acm].

  • TIP: tons of inductive problems with Koen Claessen, Moa Johansson, Dan Rosén. CICM 2015. [pdf | springer | website].

  • Hipster: integrating theory exploration in a proof assistant, with Moa Johansson, Dan Rosén, Koen Claessen. CICM 2014 (awarded best paper, Calculemus track). [pdf | springer | arxiv | website].

  • An expressive semantics of mocking, with Josef Svenningsson, Hans Svensson, Thomas Arts, Ulf Norell, John Hughes. FASE 2014. [pdf | tech report | Agda source code | springer].

  • Encoding monomorphic and polymorphic types, with Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu. TACAS 2013.
    [pdf | draft report | springer]. Extended version in my PhD thesis.

  • Automating inductive proofs using theory exploration (a.k.a. HipSpec), with Koen Claessen, Moa Johansson, Dan Rosén. CADE 2013.
    [pdf | springer]. Also in my PhD thesis.

  • Accelerating race condition detection through procrastination, with Thomas Arts, John Hughes, Ulf Norell, Hans Svensson. Erlang Workshop 2011.
    [pdf | acm]. Extended version in my PhD thesis.

  • Sort it out with monotonicity: translating between many-sorted and unsorted first-order logic (a.k.a. monkeys and bananas), with Koen Claessen, Ann Lillieström. CADE 2011.
    [pdf | springer | website]. Also in my PhD thesis.
    Note: In the published version of the paper, Lemma 3 is false. The proof of Theorem 1 is incorrect, although the theorem itself is true. For a corrected version, see my PhD thesis.

  • QuickSpec: guessing formal specifications using testing, with Koen Claessen, John Hughes. Tests and Proofs 2010.
    [pdf | acm | website]. Extended version in my PhD thesis.

  • Ranking programs using black box testing, with Koen Claessen, John Hughes, Michał Pałka, Hans Svensson. Automation of Software Test 2010.
    [pdf | acm]. Extended version in my lic.

  • Finding race conditions in Erlang with QuickCheck and PULSE, with Thomas Arts, Koen Claessen, John Hughes, Michał Pałka, Hans Svensson, Ulf Wiger. ICFP 2009.
    [pdf | acm]. Extended version in my PhD thesis.

Some software

A couple of old links