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