Dr. rer. nat. Joachim Breitner

	Contact Email: Bitte warten...

Research interests

I mostly work on the field of Functional Programming, especially Haskell, and don’t mind some side-looks into formal verficiation and theorem proving.

Current Position

I have moved on and taken a post-doc position at the University of Pennsylvania in Philadelphia, where I have a institutional webpage. You might also be interested in my private website.

Activitis

• Program Committee Chair of Haskell in Leipzig 2016.
• Program Committee Member of Haskell Implementors Workshop 2016.
• Reviewer for AMS

Courses

• Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2016, Bestes Praktikum
• Lecture: Semantics of programming languages , Sommersemester 2015, Beste Wahlvorlesung
• Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2013, Bestes Praktikum
• Common Excercises: Tutorial for Semantics of programming languages , Sommersemester 2012

Publications

2018

• Illi Isabellistes Se Custodes Egregios Praestabant
  Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday 2018, pp. 267--282 : S. Bischof, J. Breitner, D. Lohner, G. Snelting
• Low-Deterministic Security For Low-Nondeterministic Programs
  Journal of Computer Security 2018, pp. 335--366 : S. Bischof, J. Breitner, J. Graf, M. Hecker, M. Mohr, G. Snelting

2017

• Der Grader Praktomat
  Automatisierte Bewertung in der Programmierausbildung 2017, pp. 159-172 : J. Breitner, M. Hecker, G. Snelting

2016

• Safe zero-cost coercions for Haskell
  Journal of Functional Programming July 2016 : J. Breitner, R. Eisenberg, S. P. Jones, S. Weirich
• Surprise Paradox
  Archive of Formal Proofs July 2016 : J. Breitner
• The meta theory of the Incredible Proof Machine
  Archive of Formal Proofs May 2016 : J. Breitner, D. Lohner
• Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
  April 2016 : J. Breitner
• On Improvements Of Low-Deterministic Security
  Principles of Security and Trust - 5th International Conference, POST 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings 2016, pp. 68--88 (POST 16) : J. Breitner, J. Graf, M. Hecker, M. Mohr, G. Snelting
• Visual theorem proving with the Incredible Proof Machine
  Interactive Theorem Proving 2016 (ITP 2016) : J. Breitner

2015

• Punktgenau -- Multimedia-Spielzeug Tiptoi selbst programmieren
  December 2015, pp. 108-114 : J. Breitner, C. Podszun
• Stiftzauber -- Eigene Bücher und Spiele für den Tiptoi vertonen
  March 2015, pp. 156-159 : J. Breitner, C. Podszun
• The Safety of Call Arity
  Archive of Formal Proofs February 2015 : J. Breitner
• Call Arity
  Trends in Functional Programming 2015, pp. 34-50 (TFP 2014) : J. Breitner
• Formally Proving a Compiler Transformation Safe
  Haskell 2015 (Haskell'15) : J. Breitner

2014

• The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
  ArXiv e-prints May 2014 : J. Breitner
• Safe Zero-cost Coercions for Haskell
  ICFP 2014 (ICFP 2014) : J. Breitner, R. Eisenberg, S. P. Jones, S. Weirich

2013

• Certified HLints with Isabelle/HOLCF-Prelude
  ArXiv e-prints June 2013 : J. Breitner, B. Huffman, N. Mitchell, C. Sternagel
• The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
  Archive of Formal Proofs January 2013 : J. Breitner

2012

• dup -- Explicit un-sharing in Haskell
  ArXiv e-prints July 2012 : J. Breitner
• Tackling the testing migration problem with SAT-Solvers
  ArXiv e-prints April 2012 : J. Breitner
• The ghc-heap-view package
  March 2012 : J. Breitner

2011

• Loop subgroups of F_r and the image of their stabilizer subgroups in GL_r(Z)
  Israel Journal of Mathematics December 2011, pp. 1-13 : J. Breitner
• The General Triangle Is Unique
  Archive of Formal Proofs April 2011 : J. Breitner

2010

• Shivers' Control Flow Analysis
  Archive of Formal Proofs November 2010 : J. Breitner
• Control Flow in Functional Languages -- Formally taming lambdas
  November 2010 : J. Breitner
• The shivers-cfg package
  November 2010 : J. Breitner
• Loop subgroups of F_r and the images of their stabilizer subgroups in GL_r(Z)
  February 2010 : J. Breitner

Projects

• PRAKTOMAT
• Quis-Custodiet
• Brunhilde

Advised thesis projects

finished

• Call Arity vs. Demand Analysis, masters thesis
• Open inductive predicates, masters thesis
• Qualitative Modelling of Biological Signalling Pathways using SAT-solving in Prolog, bachelor thesis
• Modeling Uncertain Data using Monads and an Application to the Sequence Alignment Problem, bachelor thesis
• Inferring equalities in functional programs, bachelor thesis
• Visualization of Lazy Evaluation and Sharing, bachelor thesis

Theses worked on

• Verifiying Shiver's functional CFA analysis (finished), study thesis

Talks and further publications can be found on my private publication page.