Publications

Academics (peer-reviewed)

• Conference paperwith Nadia HeningerBiased Nonce Sense: Lattice Attacks against Weak ECDSA Signatures in Cryptocurrencies2019, Financial Cryptography and Data Security 2019,
  Preprint: ePrint:2019/023
• Journal paperwith Simon Bischof, Denis Lohner & Gregor SneltingIlli Isabellistes Se Custodes Egregios Praestabant2018, Principled Software Development, Springer,
  DOI: 10.1007/978-3-319-98047-8_17
• Conference paperA promise checked is a promise kept: Inspection Testing2018, Haskell 2018,
  DOI: 10.1145/3242744.3242748 • Preprint: arXiv:1803.07130
• Conference paperwith Richard A. Eisenberg & Simon Peyton JonesType variables in patterns2018, Haskell 2018,
  DOI: 10.1145/3242744.3242753 • Preprint: arXiv:1806.03476
• Conference paperwith Niki Vazou, Will Kunkel, David Van Horn & Graham HuttonFunctional Pearl: Theorem Proving for AllEquational Reasoning in Liquid Haskell2018, Haskell 2018,
  DOI: 10.1145/3242744.3242756 • Preprint: arXiv:1806.03541
• Conference paperwith Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley & Stephanie WeirichReady, Set, Verify! Applying hs-to-coq to real-world Haskell code (Experience Report)2018, ICFP 2018,
  DOI: 10.1145/3236784 • Preprint: arXiv:1803.06960
• Journal paperThe Adequacy of Launchbury's Natural Semantics for Lazy Evaluation2018, 3.1.2017, Journal of Functional Programming, Volume 28,
  DOI: 10.1017/S0956796817000144 • Preprint: arXiv:1405.3099
• Conference paperwith Antal Spector-Zabusky, Christine Rizkallah & Stephanie WeirichTotal Haskell is Reasonable Coq2017, CPP 2018,
  DOI: 10.1145/3167092 • Preprint: arXiv:1711.09286
• 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,
  DOI: 10.1007/978-3-319-66787-4_27 • Preprint: ePrint:2017/627
• Conference paperwith Chris SmithLock-step simulation is child's playExperience Report29.8.2017, ICFP 2017,
  DOI: 10.1145/3110247 • PDF-File • Preprint: arXiv:1705.09704
• Conference paperwith Marco Vassena & Alejandro RussoSecuring Concurrent Lazy Programs Against Information LeakageAugust2017, CSF 2017,
  DOI: 10.1109/CSF.2017.39 • PDF-File
• Journal paperCall Arity14.3.2017, Computer Languages, Systems & Structures (COMLAN),
  DOI: 10.1016/j.cl.2017.03.001
• 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,
  DOI: 10.1017/S0956796817000016
• Journal paperwith Richard Eisenberg, Simon Peyton Jones & Stephanie WeirichSafe zero-cost coercions for Haskell28.7.2016, Journal of Functional Programming, Volume 26,
  DOI: 10.1017/S0956796816000150
• Conference paperVisual theorem proving with the Incredible Proof Machine7.8.2016, ITP 2016,
  PDF-File • DOI: 10.1007/978-3-319-43144-4_8
• Conference paperwith Jürgen Graf, Martin Hecker, Martin Mohr & Gregor SneltingOn Improvements Of Low-Deterministic Security2016, POST,
  PDF-File • DOI: 10.1007/978-3-662-49635-0_4
• Conference paperFormally Proving a Compiler Transformation Safe30.8.2015, Haskell Symposium,
  DOI: 10.1145/2804302.2804312 • PDF-File
• Conference paperCall Arity27.12.2014, Trends in Functional Programming, LNCS, Springer, Best student paper award,
  DOI: 10.1007/978-3-319-14675-1_3 • PDF-File
• Conference paperwith Richard Eisenberg, Simon Peyton Jones & Stephanie WeirichSafe Zero-cost Coercions for Haskell28.2.2014, ICFP 2014,
  DOI: 10.1145/2628136.2628141 • PDF-File
• Journal paperLoop subgroups of F_r and the image of their stabilizer subgroups in GL_r(ℤ)Israel Journal of Mathematics, 21.12.2011, Issue 45, Pages 16-28,
  DOI: 10.1007/s11856-011-0213-3 • Preprint: arXiv:1012.2729

Academics (non peer-reviewed)

• Workshop paperDemo: Kaleidogen2017, FARM,
  Event Schedule • PDF-File
• Preprint More on sliding right28.11.2018,
  Preprint: ePrint:2018/1163
• Preprintwith Maciej SkórskiAnalytic Formulas for Renyi Entropy of Hidden Markov Models2018,
  Preprint: arXiv:1709.09699
• Workshop paperThe sufficiently smart compiler is a theorem prover2017, IFL 2017 preproceedings,
  Event Schedule • PDF-File • Preprint: arXiv:1805.08106
• Book chapterwith Martin Hecker & Gregor SneltingDer Grader Praktomat2017, Automatisierte Bewertung in der Programmierausbildung,
  978-3-8309-3606-0 • Homepage • German National Library entry
• Workshop paperwith Marco Vassena & Alejandro RussoSecuring Concurrent Lazy Programs 23.4.2017, 5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017),
  Event Schedule • PDF-File
• Workshop paperCall Arity17.3.2014, TFP 2014 preproceedings,
  PDF-File
• Workshop paperwith Brian Huffman, Neil Mitchell & Christian SternagelCertified HLints with Isabelle/HOLCF-Prelude6.6.2013,
  Preprint: arXiv:1306.1340
• Preprintdup – Explicit un-sharing in Haskell9.8.2012,
  Preprint: arXiv:1207.2017
• PreprintTackling the testing migration problem with SAT-Solvers13.4.2012,
  Preprint: arXiv:1204.2974
• PreprintConditional Elimination through Code Duplication15.6.2011,
  Preprint: arXiv:1106.3478

Formal Proofs (peer-reviewed)

• Isabelle Proof Theorywith Brian Huffman, Neil Mitchell & Christian SternagelHOLCF-PreludeThe Archive of Formal Proofs, 15.7.2017,
  Journal entry
• Isabelle Proof TheorySurprise ParadoxThe Archive of Formal Proofs, Issue July, 17.7.2016,
  Journal entry
• Isabelle Proof Theorywith Denis LohnerThe meta theory of the Incredible Proof MachineThe Archive of Formal Proofs, 20.5.2016,
  Journal entry
• Isabelle Proof TheoryThe Safety of Call ArityThe Archive of Formal Proofs, 20.2.2015,
  Journal entry
• Isabelle Proof TheoryThe Correctness of Launchbury's Natural Semantics for Lazy EvaluationThe Archive of Formal Proofs, 31.1.2013,
  Journal entry
• Isabelle Proof TheoryShivers’ Control Flow AnalysisThe Archive of Formal Proofs, 16.11.2010,
  Journal entry
• Isabelle Proof TheoryThe General Triangle Is UniqueThe Archive of Formal Proofs, 1.4.2011,
  Journal entry
• Isabelle Proof TheoryFree GroupsThe Archive of Formal Proofs, 24.6.2010,
  Journal entry

Theses

• Doctoral ThesisLazy Evaluation: From natural semantics to a machine-checked compiler transformation2016, Karlsruhe Institute of Technology,
  DOI: 10.5445/IR/1000054251 • Website
• Student research projectControl Flow in Functional LanguagesFormally taming lambdas2010, Karlsruhe Institute of Technology,
  PDF-File • Blog entry
• Diploma thesisLoop subgroups of F_r and the images of their stabilizer groups in GL_r(ℤ)2010, Karlsruhe Institute of Technology,
  PDF-File • LaTeX-Source • Blog entry

Talks

• TalkThe many faces of isOrderedTree7.9.2019, MuniHac, Munich,
  Event Schedule • Video Stream
• TalkDemo: Kaleidogen23.8.2019, FARM,
  Event Schedule
• TalkDen Tiptoi-Stift hacken6.4.2019, Linux-Informations-Tag, Augsburg,
  Event Schedule • Video Stream
• TalkA Promise Checked Is a Promise Kept: Inspection Testing22.3.2019, BobKonf 2019, Berlin,
  Event Schedule • Video Stream
• TalkA Promise Checked Is a Promise Kept: Inspection Testing3.10.2018, Haskell eXchange, London,
  Event Schedule • Video Stream
• 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,
  Event Schedule
• TalkA Promise Checked Is a Promise Kept: Inspection Testing28.9.2018, Haskell Symposium 2018, Saint Louis,
  Event Schedule
• TalkReady, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report)26.9.2018, ICFP 2018, Saint Louis,
  Event Schedule • Slides • Video Stream
• 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,
  Event Schedule • Video Stream
• 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,
  Event Schedule • Slides
• TalkHaskell20.1.2018, PennApps, Philadelphia,
  Event Schedule • Slides
• TalkDeferred Termination Proofs8.1.2018, LMU Müchen
• TalkBeyond correct and fast: Inspection Testing4.12.2017, IBM PL Day, Yorktown Heights, NY,
  Event Schedule
• TalkBeyond correct and fast: Inspection Testing17.11.2017, University of Maryland – Programming Languages Group, College Park,
  Event Schedule
• Guest lectureHaskell Bytes16.11.2017, CMSC 498V - Advanced Functional Programming by Niki Vazou, University of Maryland, College Park,
  Event Schedule
• TalkThe sufficiently smart compiler can prove theorems!8.9.2019, WPTE 2017, Oxford, Invited talk,
  Event Schedule
• TalkLock-step simulation is child's play4.9.2017, ICFP 2017, Oxford,
  Event Schedule • Slides • Video Stream
• 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,
  Event Schedule • Slides • Blog entry
• TalkLock-step simulation is child's play26.5.2017, University of Pennsylvania – PL Club, Philadelphia,
  Slides
• TalkLock-step simulation is child's play18.5.2017, Compose :: Conference, New York City,
  Event Schedule • Slides • Video Stream
• TalkWho needs theorem provers when we have compilers?3.5.2017, Haskell User Group, Paris,
  Event Schedule
• 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,
  Event Schedule • Video Stream
• 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,
  Event Schedule • Slides
• 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,
  Event Schedule • Transcript • DOI: 10.1145/2966268.2966273
• Talkwith Sebastian GrafCommits statt ZeitDas git-gewahre Performance-Dashboard gipeda28.5.2016, Gulaschprogrammiernacht 16, Karlsruhe,
  Event Schedule • Video Stream
• TalkHaskell für Mathematiker12.5.2016, AG Seminar Topology, Karlsruhe,
  Event Schedule • Slides
• TalkCall Arity29.2.2016, InfSec group seminar, ETH, Zürich,
  Event Schedule
• TalkMit Monaden die Zukunft im Blick19.2.2016, BobKonf 2016, Berlin,
  Event Schedule • Transcript • Video Stream
• TutorialVerifikation mit Isabelle19.2.2016, BobKonf 2016, Berlin,
  Event Schedule • Handout • Slides
• TalkMit Monaden die Zukunft im Blick4.12.2015, HaL10, Leipzig, Invited talk,
  Event Schedule • Transcript
• TutorialBeweisführung in der Mathematik9.-11.10.2015, MINT-Forscherwerkstatt der START-Stipendiaten, Jülich,
  Blog entry
• TalkDer Tiptoi-Stift6.6.2015, Gulaschprogrammiernacht 15, Karlsruhe,
  Event Schedule • Slides • Video Stream
• TalkFormally Proving a Compiler Transformation Safe3.9.2015, Haskell Symposium 2015, Vancouver,
  Event Schedule • Video Stream • Slides
• TalkMonads for Reverse Engineering15.4.2015, The Karlsruhe Functional Programmers Meetup Group, Karlsruhe,
  Event Schedule • Blog entry
• TalkThe proof assistant Isabelle27.11.2014, Computer Tools for Pure Mathematics, Freiburg,
  Event Schedule
• TalkContributing to GHC6.9.2014, Haskell Implementors Workshop, Gothenburg, Sweden,
  Event Schedule • Slides • Video Stream
• TalkHaskell in DebianThe what, the how, and the what now?28.8.2014, DebConf 14, Portland, Oregon, USA,
  Event Schedule • Slides
• TalkHaskell BytesA guided tour through the heap of a Haskell program13.6.2014, Galois Tech Talk, Portland,
  Transcript • Video Stream
• TalkCall Arity27.5.2014, TFP 2014, Soesterburg, The Netherlands,
  Event Schedule • Slides
• 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,
  Transcript
• TalkHaskell und Debian21.6.2013, HaL8, Leipzig,
  Event Schedule • PDF-File
• TalkAgda – mit starken Typen abhängen15.5.2013, The Karlsruhe Functional Programmers Meetup Group, Karlsruhe,
  Event Schedule
• 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,
  Transcript
• TalkA Haskell Roadshow18.12.2012, The Karlsruhe Functional Programmers Meetup Group, Karlsruhe,
  Event Schedule • Transcript • Slides
• TalkHaskell BytesEine geführte Tour durch den Hauptspeicher eines Haskell-Programms8.9.2012, MRMCD 12, Darmstadt,
  Event Schedule • Transcript
• TalkAgda – Mit starken Typen abhängenEine Demo der abhängig getypten Programmiersprache7.6.2012, Gulaschprogrammiernacht 12, Karlsruhe,
  Event Schedule • Slides
• Guest lectureEine nicht ganz faule ShowPerformance in Haskell6.12.2011, Vorlesung Fortgeschrittene Funktionale Programmierung von Jun.-Prof. Dr. Janis Voigtländer, Bonn,
  Transcript • Blog entry
• TalkHaskell in Debian28.7.2011, DebConf 11, Banja Luka, Bosnien-Herzegovina,
  Event Schedule • Slides • Video Stream
• TalkWarum wir noch Mathematiker brauchenChurch und das Entscheidungsproblem24.6.2011, Gulaschprogrammiernacht 11, Karlsruhe,
  Event Schedule • Transcript • Video Stream
• TalkChurch’s undecidability result21.4.2011, Alan Turing Birth Centennial Talk, IIT Bombay, Mumbai,
  Transcript
• TalkA Haskell Roadshow11.2.2011, GNUnify 2011, Pune, Indien,
  Slides • Blog entry
• TalkMonaden in Haskell16.11.2010, Seminar Kategorientheorie, Karlsruhe,
  Event Schedule • Handout
• TalkSchleifenuntergruppen von F_r und die Bilder ihrer Stabilisatorgruppen in GL_r(ℤ)11.3.2010, Studierendenkonferenz der Deutschen Mathematiker-Vereinigung, München,
  Event Schedule
• Talkzpub: Ein Redaktionsprozess auf Basis von OpenSource-Software9.3.2010, tfk Technologietag 2010, München,
  Event Schedule • Slides
• TalkUpstream-nahe Weiterentwicklung Freier Software3.3.2010, CeBIT Open Source Forum 2010, Hannover,
  Event Schedule • Video Stream
• TalkFreie Werkzeuge für die technische Dokumentation14.2.2010, 3. Anwenderkreis Open Source im Maschinenbau, Stuttgart,
  Event Schedule • Slides
• TalkLoop subgroups of F_r and the images of their stabilizer groups in GL_r(ℤ)15.12.2009, Siebter Karlsruher Weihnachtsworkshop zur Geometrie und Zahlentheorie,
  Event Schedule
• TalkDistributing virtually boxed applications.vdi to .deb28.7.2009, DebConf 9, Cáceres,
  Slides • Event Schedule

Magazines etc.

• Articlewith Carsten PodszunPunktgenauMultimedia-Spielzeug Tiptoi selbst programmierenMake:, Issue 06, 2015, Pages 108-114,
  Online Article
• Articlewith Carsten PodszunStiftzauberEigene Bücher und Spiele für den Tiptoi vertonenc't, Issue 08, 2015,
  Blog entry • Online Article
• PaperProblem 4Graph Theory Problem PoetryEulenspiegel, Issue 48, Page 4, 12.1.2013,
  Online Article
• ArticleIIT Bombay’s Affirmative ActionRaintree-Magazin, Issue 10-11, 2011, Page 8,
  Online Article • Blog entry
• PaperWürfeln mit WubbelEulenspiegel, Issue 45, Pages 16-28, 12.5.2011,
  Online Article
• 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,
  Blog entry • Online Article
• ArticleFontásticoFuentes de símbolos caseras con FontForgeLinux Magazine, Issue 62, 2010, Pages 71-73,
  Online Article
• ArticleThe Light FontasticDo-it-yourself symbol fonts with FontForgeLinux Magazine, Issue 113, 2010
• ArticleSchrift-SchmiedeSymbolschriften mit Fontforge selbst gemachtLinux-Magazin, Issue 03, 2010,
  Online Article • Blog entry
• ArticleWindows-Installation mit apt-getfreeX, Issue 1, 2010, Pages 32-35,
  Blog entry
• ArticleUn Pez Llamado PhishingPara los Ataques de Autentición MultiplataformasLinux Magazine, Issue 13, 2005, Pages 44-45,
  Online Article
• ArticleStrange PhishingStopping the cross-site authentication attackLinux Magazine, Issue 40, 2005, Pages 42-43,
  Online Article • Blog entry
• ArticleVerführerische BildchenEinfaches Passwort-Phishing durch eingebettete Bilder: Cross-Site-Authentication-AttackenLinux-Magazin, Issue 10, 2005,
  Online Article • Blog entry

Podcasts

• PodcastIncredible Proof MachineGespräch mit Sebastian Ritterbusch im Modellansatz PodcastEpisode 78, 2016,
  Website
• PodcastPapierrechnerGespräch mit Sebastian Ritterbusch im Modellansatz PodcastEpisode 47, 2015,
  Website

Books

• BookLazy Evaluation: From natural semantics to a machine-checked compiler transformation2016,
  9783731505464 • DOI: 10.5445/KSP/1000056002 • Homepage • PDF-File • German National Library entry
• 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,
  Homepage • German National Library entry