Publications

Navigation

Academics (peer-reviewed)

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
Isabelle Proof TheorySurprise ParadoxThe Archive of Formal Proofs, Issue July, 2016,
Journal entry
PaperVisual theorem proving with the Incredible Proof Machine2016, ITP,
PDF-File • DOI: 10.1007/978-3-319-43144-4_8 • Slides
Isabelle Proof Theorywith Denis LohnerThe meta theory of the Incredible Proof MachineThe Archive of Formal Proofs, Issue May, 2016,
Journal entry
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
PaperFormally Proving a Compiler Transformation Safe2015, Haskell Symposium,
DOI: 10.1145/2804302.2804312 • PDF-File • Video Stream
Isabelle Proof TheoryThe Safety of Call ArityThe Archive of Formal Proofs, Issue January, 2015,
Journal entry
PaperCall Arity2015, Trends in Functional Programming, LNCS, Springer, Best student paper award,
DOI: 10.1007/978-3-319-14675-1_3 • PDF-File
Paperwith Richard Eisenberg, Simon Peyton Jones & Stephanie WeirichSafe Zero-cost Coercions for Haskell28.2.2014, ICFP 2014,
DOI: 10.1145/2628136.2628141 • PDF-File
Isabelle Proof TheoryThe Correctness of Launchbury's Natural Semantics for Lazy EvaluationThe Archive of Formal Proofs, Issue January, 2013,
Journal entry
PaperShivers’ Control Flow AnalysisA formalization with Isabelle/HOLThe Archive of Formal Proofs, Issue November, 2010,
Journal entry
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
Isabelle Proof TheoryThe General Triangle Is UniqueA formalization with Isabelle/HOLThe Archive of Formal Proofs, Issue April, 2011,
Journal entry
Isabelle Proof TheoryFree GroupsA formalization with Isabelle/HOLThe Archive of Formal Proofs, Issue June, 2010,
Journal entry

Go up

Academics (non peer-reviewed)

PaperThe Correctness of Launchbury's Natural Semantics for Lazy Evaluation13.5.2014,
Preprint: arXiv:1405.3099
PaperCall Arity17.3.2014, TFP 2014 preproceedings,
PDF-File
Paperwith Brian Huffman, Neil Mitchel and Christian SternagelCertified HLints with Isabelle/HOLCF-Prelude6.6.2013,
Preprint: arXiv:1306.1340
Paperdup – Explicit un-sharing in Haskell9.8.2012,
Preprint: arXiv:1207.2017
PaperTackling the testing migration problem with SAT-Solvers13.4.2012,
Preprint: arXiv:1204.2974
PaperConditional Elimination through Code Duplication15.6.2011,
Preprint: arXiv:1106.3478

Go up

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

Go up

Talks

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
TalkVerifikation 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
TalkDer Tiptoi-Stift6.6.2015, Gulaschprogrammiernacht 15, Karlsruhe,
Event Schedule • Slides • Video Stream
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
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
TalkHaskell BytesEine geführte Tour durch den Hauptspeicher eines Haskell-Programms10.1.2013, Gastvortrag in der 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
TalkEine nicht ganz faule ShowPerformance in Haskell6.12.2011, Gastvortrag in der 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

Go up

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

Go up

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

Go up

Books

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

Go up