Publications
Academics (peer-reviewed)
- Conference paperwith Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Philippa Gardner, Sam Lindley, Matija Pretnar, Rao Xiaojia, Conrad Watt & Andreas RossbergBringing the WebAssembly Standard up to Speed with SpecTec2024, PLDI 2024,
- Conference paperMore fixpoints!Functional Pearl2023, ICFP 2023,
- Conference paperwith Lennart Augustsson, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele Jr. & Tim SweeneyThe Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming2023, ICFP 2023,
- Conference paperwith Dylan Rowe & Nadia HeningerThe curious case of the half-half Bitcoin ECDSA nonces2023, AfricaCrypt 2023,
- Journal paperwith Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen & Stephanie WeirichReady, Set, Verify! Applying hs-to-coq to real-world Haskell code2021, Journal of Functional Programming, Volume 31,
- Conference paperwith Maciej SkórskiExplicit Renyi Entropy for Hidden Markov Models2020, ISIT 2020,
- Conference paperwith Nadia HeningerBiased Nonce Sense: Lattice Attacks against Weak ECDSA Signatures in Cryptocurrencies2019, Financial Cryptography and Data Security 2019,
- Journal paperwith Simon Bischof, Denis Lohner & Gregor SneltingIlli Isabellistes Se Custodes Egregios Praestabant2018, Principled Software Development, Springer,
- Conference paperA promise checked is a promise kept: Inspection Testing2018, Haskell 2018,
- Conference paperwith Richard A. Eisenberg & Simon Peyton JonesType variables in patterns2018, Haskell 2018,
- Conference paperwith Niki Vazou, Will Kunkel, David Van Horn & Graham HuttonFunctional Pearl: Theorem Proving for AllEquational Reasoning in Liquid Haskell2018, Haskell 2018,
- Conference paperwith Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley & Stephanie WeirichReady, Set, Verify! Applying hs-to-coq to real-world Haskell codeExperience Report2018, ICFP 2018,
- Journal paperThe Adequacy of Launchbury's Natural Semantics for Lazy Evaluation2018, 3.1.2017, Journal of Functional Programming, Volume 28,
- Conference paperwith Antal Spector-Zabusky, Christine Rizkallah & Stephanie WeirichTotal Haskell is Reasonable Coq2017, CPP 2018,
- Conference paperwith Daniel J. Bernstein, Daniel Genkin, Leon Groot Bruinderink, Nadia Heninger, Tanja Lange, Christine van Vredendaal & Yuval YaromSliding right into disaster: Left-to-right sliding windows leak25.8.2017, CHES 2017,
- Conference paperwith Chris SmithLock-step simulation is child's playExperience Report29.8.2017, ICFP 2017,
- Conference paperwith Marco Vassena & Alejandro RussoSecuring Concurrent Lazy Programs Against Information LeakageAugust2017, CSF 2017,
- Journal paperCall Arity14.3.2017, Computer Languages, Systems & Structures (COMLAN),
- Journal paperwith Ilya Sergey, Dimitrios Vytiniotis & Simon Peyton JonesModular, higher order cardinality analysis in theory and practice16.2.2017, Journal of Functional Programming, Volume 27,
- Journal paperwith Richard Eisenberg, Simon Peyton Jones & Stephanie WeirichSafe zero-cost coercions for Haskell28.7.2016, Journal of Functional Programming, Volume 26,
- Conference paperVisual theorem proving with the Incredible Proof Machine7.8.2016, ITP 2016,
- Conference paperwith Jürgen Graf, Martin Hecker, Martin Mohr & Gregor SneltingOn Improvements Of Low-Deterministic Security2016, POST,
- Conference paperFormally Proving a Compiler Transformation Safe30.8.2015, Haskell Symposium,
- Conference paperCall Arity27.12.2014, Trends in Functional Programming, LNCS, Springer, Best student paper award,
- Conference paperwith Richard Eisenberg, Simon Peyton Jones & Stephanie WeirichSafe Zero-cost Coercions for Haskell28.2.2014, ICFP 2014,
- Journal paperLoop subgroups of Fr and the image of their stabilizer subgroups in GLr(ℤ)Israel Journal of Mathematics, 21.12.2011, Issue 45, Pages 16-28,
Academics (non peer-reviewed)
- Preprintwith Matthew Bolan, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber & Fan ZhenThe Equational Theories Project: Advancing Collaborative Mathematical Research at Scale2025,
- Workshop paperDemo: Kaleidogen2017, FARM,
- PreprintMore on sliding right28.11.2018,
- Workshop paperThe sufficiently smart compiler is a theorem prover2017, IFL 2017 preproceedings,
- Book chapterwith Martin Hecker & Gregor SneltingDer Grader Praktomat2017, Automatisierte Bewertung in der Programmierausbildung,
- Workshop paperwith Marco Vassena & Alejandro RussoSecuring Concurrent Lazy Programs 23.4.2017, 5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017),
- Workshop paperCall Arity17.3.2014, TFP 2014 preproceedings,
- Workshop paperwith Brian Huffman, Neil Mitchell & Christian SternagelCertified HLints with Isabelle/HOLCF-Prelude6.6.2013,
- Preprintdup – Explicit un-sharing in Haskell9.8.2012,
- PreprintTackling the testing migration problem with SAT-Solvers13.4.2012,
- PreprintConditional Elimination through Code Duplication15.6.2011,
Formal Proofs (peer-reviewed)
- Isabelle Proof Theorywith Brian Huffman, Neil Mitchell & Christian SternagelHOLCF-PreludeThe Archive of Formal Proofs, 15.7.2017,
- Isabelle Proof TheorySurprise ParadoxThe Archive of Formal Proofs, Issue July, 17.7.2016,
- Isabelle Proof Theorywith Denis LohnerThe meta theory of the Incredible Proof MachineThe Archive of Formal Proofs, 20.5.2016,
- Isabelle Proof TheoryThe Safety of Call ArityThe Archive of Formal Proofs, 20.2.2015,
- Isabelle Proof TheoryThe Correctness of Launchbury's Natural Semantics for Lazy EvaluationThe Archive of Formal Proofs, 31.1.2013,
- Isabelle Proof TheoryShivers’ Control Flow AnalysisThe Archive of Formal Proofs, 16.11.2010,
- Isabelle Proof TheoryThe General Triangle Is UniqueThe Archive of Formal Proofs, 1.4.2011,
- Isabelle Proof TheoryFree GroupsThe Archive of Formal Proofs, 24.6.2010,
Theses
- Doctoral ThesisLazy Evaluation: From natural semantics to a machine-checked compiler transformation2016, Karlsruhe Institute of Technology,
- Student research projectControl Flow in Functional LanguagesFormally taming lambdas2010, Karlsruhe Institute of Technology,
- Diploma thesisLoop subgroups of Fr and the images of their stabilizer groups in GLr(ℤ)2010, Karlsruhe Institute of Technology,
Talks
- TalkLean Highlights31.10.2025, University of Pennsylvania – PL Club, Philadelphia,
- TalkReport from the FRO2.10.2025, Lean workshop at ITP, Reykjavik,
- TalkRecursive Definitions in Lean15.8.2025, Computer Laboratory Computer Architecture Group Meeting, Cambridge,
- Tutorialwith Sebastian UllrichThe Lean Programming Language and Theorem Prover12.8.2025, VeTSS Summer School 2024, Glasgow,
- TalkRecursive Definitions in Lean14.3.2025, BobConf 2025, Berlin,
- TalkRecursive Definitions in Lean13.3.2025, Leaning in 2025, Berlin,
- Tutorialwith Sebastian UllrichThe Lean Programming Language and Theorem Prover13.10.2024, VSTTE 2024, Prague,
- Tutorialwith David Thrane ChristiansenLean for the Functional Programmer15.3.2024, BobConf 2024, Berlin,
- TalkMore Fixpoints!Functional Pearl5.9.2023, ICFP 2023, Seattle,
- TalkGetting recursive definitions off their bottoms17.3.2023, BobConf 2023, Berlin,
- TalkGetting recursive definitions off their bottoms7.10.2022, MuniHac, Munich,
- TalkBiased Nonce Sense20.5.2022, GPN20, Karlsruhe,
- TutorialSpecification-driven design11.3.2022, BobKonf 2022, virtual,
- TalkA sound higher-order interface description language21.9.2021, Verified Systems Engineering seminar, NUS (virtual),
- TalkThe Internet Computer14.9.2021, Digital Asset, Zürich
- TalkWinter is Coming – Even Faster26.3.2021, University of Pennsylvania – PL Club, virtual
- TutorialHaskell Bytes26.2.2018, BobKonf 2021, virtual,
- TalkWinter is Coming – Even Faster4.11.2020, Haskell eXchange, Virtual,
- TalkThe many faces of isOrderedTree31.7.2020, Haskell Love, Virtual,
- TalkMotoko21.2.2020, Stanford Blockchain Conference, Palo Alto,
- TalkBiased Nonce Sense16.2.2020, Silicon Valley Ethereum Meetup, Palo Alto,
- TalkThe many faces of isOrderedTree7.9.2019, MuniHac, Munich,
- TalkDemo: Kaleidogen23.8.2019, FARM,
- TalkDen Tiptoi-Stift hacken6.4.2019, Linux-Informations-Tag, Augsburg,
- TalkA Promise Checked Is a Promise Kept: Inspection Testing22.3.2019, BobKonf 2019, Berlin,
- TalkA Promise Checked Is a Promise Kept: Inspection Testing3.10.2018, Haskell eXchange, London,
- TalkA Promise Checked Is a Promise Kept: Inspection Testing8.10.2018, Microsoft Research PL Lunch Talk, Cambridge, UK
- TalkA Promise Checked Is a Promise Kept: Inspection Testing3.10.2018, Haskell Hackers: The South SF Bay Haskell User Group, Sunnyvale,
- TalkA Promise Checked Is a Promise Kept: Inspection Testing28.9.2018, Haskell Symposium 2018, Saint Louis,
- TalkReady, Set, Verify! Applying hs-to-coq to Real-World Haskell CodeExperience Report26.9.2018, ICFP 2018, Saint Louis,
- TalkA promise checked is a promise kept: Inspection Testing29.6.2018, University of Pennsylvania – PL Club, Philadelphia
- TalkA promise checked is a promise kept: Inspection Testing9.6.2018, ZuriHac, Zurich,
- TalkWozu Theorembeweiser, wenn wir Compiler haben?25.5.2018, 60th anniversary of Prof. Gregor Snelting, Karlsruhe
- TalkLock-step simulation is child's play9.3.2018, Comcast Labs Connect Functional Programming Conference, Philadelphia,
- TalkHaskell20.1.2018, PennApps, Philadelphia,
- TalkDeferred Termination Proofs8.1.2018, LMU Müchen
- TalkBeyond correct and fast: Inspection Testing4.12.2017, IBM PL Day, Yorktown Heights, NY,
- TalkBeyond correct and fast: Inspection Testing17.11.2017, University of Maryland – Programming Languages Group, College Park,
- Guest lectureHaskell Bytes16.11.2017, CMSC 498V - Advanced Functional Programming by Niki Vazou, University of Maryland, College Park,
- TalkThe sufficiently smart compiler can prove theorems!8.9.2019, WPTE 2017, Oxford, Invited talk,
- TalkLock-step simulation is child's playExperience Report4.9.2017, ICFP 2017, Oxford,
- TalkThe sufficiently smart compiler is a theorem prover30.8.2017, IFL 2017, Bristol
- TalkLock-step simulation is child's play22.6.2017, Haskell Hackers: The South SF Bay Haskell User Group, Sunnyvale,
- TalkLock-step simulation is child's play26.5.2017, University of Pennsylvania – PL Club, Philadelphia,
- TalkLock-step simulation is child's play18.5.2017, Compose :: Conference, New York City,
- TalkWho needs theorem provers when we have compilers?3.5.2017, Haskell User Group, Paris,
- TalkWho needs theorem provers when we have compilers?2.5.2017, Seminar “Analyse et conception de systèmes”, Institut de Recherche en Informatique Fondamentale, Université Paris-Diderot, Paris, Event Schedule
- TalkWho needs theorem provers when we have compilers?9.3.2017, HaskellerZ, Zürich,
- TalkWho needs theorem provers when we have compilers?1.3.2017, Programming Systems PL Lunch, University of California – San Diego
- TalkCall Arity13.9.2016, University of Pennsylvania – PL Club, Philadelphia
- TalkVisual theorem proving with the Incredible Proof Machine22.8.2016, ITP 2016, Nancy,
- TalkVisual theorem proving with the Incredible Proof Machine19.8.2016, University of Pennsylvania – PL Club, Philadelphia
- TalkThe Incredible Proof Machine23.6.2016, LFMTP 2016, Porto, Invited talk,
- Talkwith Sebastian GrafCommits statt ZeitDas git-gewahre Performance-Dashboard gipeda28.5.2016, Gulaschprogrammiernacht 16, Karlsruhe,
- TalkHaskell für Mathematiker12.5.2016, AG Seminar Topology, Karlsruhe,
- TalkCall Arity29.2.2016, InfSec group seminar, ETH, Zürich,
- TalkMit Monaden die Zukunft im Blick19.2.2016, BobKonf 2016, Berlin,
- TutorialVerifikation mit Isabelle19.2.2016, BobKonf 2016, Berlin,
- TalkMit Monaden die Zukunft im Blick4.12.2015, HaL10, Leipzig, Invited talk,
- TutorialBeweisführung in der Mathematik9.-11.10.2015, MINT-Forscherwerkstatt der START-Stipendiaten, Jülich,
- TalkDer Tiptoi-Stift6.6.2015, Gulaschprogrammiernacht 15, Karlsruhe,
- TalkFormally Proving a Compiler Transformation Safe3.9.2015, Haskell Symposium 2015, Vancouver,
- TalkMonads for Reverse Engineering15.4.2015, The Karlsruhe Functional Programmers Meetup Group, Karlsruhe,
- TalkThe proof assistant Isabelle27.11.2014, Computer Tools for Pure Mathematics, Freiburg,
- TalkContributing to GHC6.9.2014, Haskell Implementors Workshop, Gothenburg, Sweden,
- TalkHaskell in DebianThe what, the how, and the what now?28.8.2014, DebConf 14, Portland, Oregon, USA,
- TalkHaskell BytesA guided tour through the heap of a Haskell program13.6.2014, Galois Tech Talk, Portland,
- TalkCall Arity27.5.2014, TFP 2014, Soesterburg, The Netherlands,
- TalkSafe Coercions in HaskellA Microsoft Research Cambridge Internship Talk10.2.2014, Cambridge
- TalkHaskell BytesEine geführte Tour durch den Hauptspeicher eines Haskell-Programms3.7.2013, fun-fr, Freiburg,
- TalkHaskell und Debian21.6.2013, HaL8, Leipzig,
- TalkAgda – mit starken Typen abhängen15.5.2013, The Karlsruhe Functional Programmers Meetup Group, Karlsruhe,
- Guest lectureHaskell BytesEine geführte Tour durch den Hauptspeicher eines Haskell-Programms10.1.2013, Vorlesung Fortgeschrittene Funktionale Programmierung von Jun.-Prof. Dr. Janis Voigtländer, Bonn,
- TalkA Haskell Roadshow18.12.2012, The Karlsruhe Functional Programmers Meetup Group, Karlsruhe,
- TalkHaskell BytesEine geführte Tour durch den Hauptspeicher eines Haskell-Programms8.9.2012, MRMCD 12, Darmstadt,
- TalkAgda – Mit starken Typen abhängenEine Demo der abhängig getypten Programmiersprache7.6.2012, Gulaschprogrammiernacht 12, Karlsruhe,
- Guest lectureEine nicht ganz faule ShowPerformance in Haskell6.12.2011, Vorlesung Fortgeschrittene Funktionale Programmierung von Jun.-Prof. Dr. Janis Voigtländer, Bonn,
- TalkHaskell in Debian28.7.2011, DebConf 11, Banja Luka, Bosnien-Herzegovina,
- TalkWarum wir noch Mathematiker brauchenChurch und das Entscheidungsproblem24.6.2011, Gulaschprogrammiernacht 11, Karlsruhe,
- TalkChurch’s undecidability result21.4.2011, Alan Turing Birth Centennial Talk, IIT Bombay, Mumbai,
- TalkA Haskell Roadshow11.2.2011, GNUnify 2011, Pune, Indien,
- TalkMonaden in Haskell16.11.2010, Seminar Kategorientheorie, Karlsruhe,
- TalkSchleifenuntergruppen von Fr und die Bilder ihrer Stabilisatorgruppen in GLr(ℤ)11.3.2010, Studierendenkonferenz der Deutschen Mathematiker-Vereinigung, München,
- Talkzpub: Ein Redaktionsprozess auf Basis von OpenSource-Software9.3.2010, tfk Technologietag 2010, München,
- TalkUpstream-nahe Weiterentwicklung Freier Software3.3.2010, CeBIT Open Source Forum 2010, Hannover,
- TalkFreie Werkzeuge für die technische Dokumentation14.2.2010, 3. Anwenderkreis Open Source im Maschinenbau, Stuttgart,
- TalkLoop subgroups of Fr and the images of their stabilizer groups in GLr(ℤ)15.12.2009, Siebter Karlsruher Weihnachtsworkshop zur Geometrie und Zahlentheorie,
- TalkDistributing virtually boxed applications.vdi to .deb28.7.2009, DebConf 9, Cáceres,
Magazines etc.
- ArticleHöher? Weiter? Schneller!Schauinsheft, 2021, Pages 28-29,
- ArticleDas tiptoi-ProjektDatenschleuder, Issue 102, 2020, Pages 0x1E-0x23
- Articlewith Carsten PodszunPunktgenauMultimedia-Spielzeug Tiptoi selbst programmierenMake:, Issue 06, 2015, Pages 108-114,
- Articlewith Carsten PodszunStiftzauberEigene Bücher und Spiele für den Tiptoi vertonenc't, Issue 08, 2015,
- PaperProblem 4Graph Theory Problem PoetryEulenspiegel, Issue 48, Page 4, 12.1.2013,
- ArticleIIT Bombay’s Affirmative ActionRaintree-Magazin, Issue 10-11, 2011, Page 8,
- PaperWürfeln mit WubbelEulenspiegel, Issue 45, Pages 16-28, 12.5.2011,
- ArticleTelefonbuch von UnixBenutzerkonten und der Name Service SwitchfreeX, Issue 5, 2010, Pages 80-83
- ArticleWider den WildwuchsTechnische Dokumentation mit Docbook und Zpub erstellenLinux-Magazin, Issue 05, 2010,
- ArticleFontásticoFuentes de símbolos caseras con FontForgeLinux Magazine, Issue 62, 2010, Pages 71-73,
- ArticleThe Light FontasticDo-it-yourself symbol fonts with FontForgeLinux Magazine, Issue 113, 2010
- ArticleSchrift-SchmiedeSymbolschriften mit Fontforge selbst gemachtLinux-Magazin, Issue 03, 2010,
- ArticleWindows-Installation mit apt-getfreeX, Issue 1, 2010, Pages 32-35,
- ArticleUn Pez Llamado PhishingPara los Ataques de Autentición MultiplataformasLinux Magazine, Issue 13, 2005, Pages 44-45,
- ArticleStrange PhishingStopping the cross-site authentication attackLinux Magazine, Issue 40, 2005, Pages 42-43,
- ArticleVerführerische BildchenEinfaches Passwort-Phishing durch eingebettete Bilder: Cross-Site-Authentication-AttackenLinux-Magazin, Issue 10, 2005,
Podcasts
- PodcastRein funktional gedachtCodeCultureEpisode 25, 2020,
- PodcastIncredible Proof MachineGespräch mit Sebastian Ritterbusch im Modellansatz PodcastEpisode 78, 2016,
- PodcastPapierrechnerGespräch mit Sebastian Ritterbusch im Modellansatz PodcastEpisode 47, 2015,
Books
- BookLazy Evaluation: From natural semantics to a machine-checked compiler transformation2016,
- Bookwith Hans-Helmut Köstlin, Elisabeth Riehm-Settgast, Heinrich Riehm, Ulrich Riehm & Irene StaevesIsaak Riehm (1799 - 1881) und seine Frau Charlotte geb. Rinck (1803 - 1884)mit ihren rund 700 Nachkommen sowie Isaaks selbstgeschriebene Lebenserinnerung : ein Familienbuch2011,