Joachim Breitner: doctoral thesis

This site contains auxillary data to Joachim Breitner’s doctoral thesis “Lazy Evaluation: From natural semantics to a machine-checked compiler transformation”, submitted on 2015-12-22, defended on 2016-04-25 and graded “summa cum laude”.

You can download a tarball containing all files contained herein, which is likely more useful if you want to reproduce the benchmarks, check the Isabelle theories etc.

The Thesis

The Benchmarks

The Isabelle theories

These are built as part of the build-all.sh script mentioned above. See the script for the individual steps.

Misc

Errata and Changes

These are relative to the published version, and already included in file above.

Bibliography

As a convenience, the bibliography of the thesis with clickable DOIs. (The bibliography keys are not always identical, as bibtex2html does not work with biblatex.):

[ABM07]
David Aspinall, Lennart Beringer, and Alberto Momigliano, Optimisation validation, Compiler Optimisation Meets Compiler Verification (COCV) 2006, ENTCS, vol. 176-3, 2007. [ DOI ]
[Abr90]
Samson Abramsky, The lazy lambda calculus, Research topics in functional programming (David A. Turner, ed.), Addison-Wesley, 1990.
[AO93]
Samson Abramsky and Chih-Hao Luke Ong, Full abstraction in the lazy lambda calculus, Information and Computation 105 (1993), no. 2. [ DOI ]
[BA06]
Sorav Bansal and Alex Aiken, Automatic generation of peephole superoptimizers, Architectural Support for Programming Languages and Operating Systems (ASPLOS), ACM, 2006. [ DOI ]
[Bal14]
Clemens Ballarin, Locales: A module system for mathematical theories, Journal of Automated Reasoning 52 (2014), no. 2. [ DOI ]
[BEPW14]
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich, Safe zero-cost coercions for Haskell, International Conference on Functional Programming (ICFP), ACM, 2014. [ DOI ]
[BHMS13]
Joachim Breitner, Brian Huffman, Neil Mitchell, and Christian Sternagel, Certified HLints with Isabelle/HOLCF-Prelude, Haskell and Rewriting Techniques (HART), 2013. [ arXiv ]
[Bir89]
Richard Simpson Bird, Algebraic identities for program calculation, Computer Journal 32 (1989), no. 2. [ DOI ]
[BKHT99]
Clem Baker-Finch, David King, Jon Hall, and Phil Trinder, An operational semantics for parallel call-by-need, Tech. Report 99/1, Faculty of Mathematics and Computing, The Open University, 1999.
[BKT00]
Clem Baker-Finch, David King, and Phil Trinder, An operational semantics for parallel lazy evaluation, International Conference on Functional Programming (ICFP), ACM, 2000. [ DOI ]
[Bre13]
Joachim Breitner, The correctness of Launchbury's natural semantics for lazy evaluation, Archive of Formal Proofs (2013). [ http ]
[Bre15a]
           , Call Arity, Trends in Functional Programming (TFP) 2014, LNCS, vol. 8843, Springer, 2015. [ DOI ]
[Bre15b]
           , Formally proving a compiler transformation safe, Haskell Symposium, ACM, 2015. [ DOI ]
[Bre15c]
           , The Adequacy of Launchbury's Natural Semantics for Lazy Evaluation, 2015, preprint, submitted to the Journal of Functional Programming. [ .pdf ]
[Bre15d]
           , The Safety of Call Arity, Archive of Formal Proofs (2015). [ http ]
[Buc15]
Sebastian Buchwald, Optgen: A generator for local optimizations, LCNS, vol. 9031, Springer, 2015. [ DOI ]
[CB13]
Charlie Curtsinger and Emery D. Berger, STABILIZER: statistically sound performance evaluation, Architectural Support for Programming Languages and Operating Systems (ASPLOS), ACM, 2013. [ DOI ]
[Chl10]
Adam Chlipala, A verified compiler for an impure functional language, Principles of Programming Languages (POPL), ACM, 2010. [ DOI ]
[CLS07]
Duncan Coutts, Roman Leshchinskiy, and Don Stewart, Stream fusion. from lists to streams to nothing at all, International Conference on Functional Programming (ICFP), ACM, 2007. [ DOI ]
[Coq04]
The Coq development team, The Coq proof assistant reference manual, LogiCal Project, 2004, Version 8.0. [ http ]
[Cou10]
Duncan Coutts, Stream fusion: Practical shortcut fusion for coinductive sequence types, Ph.D. thesis, University of Oxford, 2010.
[DL07]
Zaynah Dargaye and Xavier Leroy, Mechanized Verification of CPS Transformations, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 4790, Springer, 2007. [ DOI ]
[Eis15]
Richard Eisenberg, System FC, as implemented in GHC, 2015. [ .pdf ]
[EM04]
Marko van Eekelen and Maarten de Mol, Mixed lazy/strict graph semantics, Tech. Report NIII-R0402, Radboud University Nijmegen, January 2004.
[FHG14]
Andrew Farmer, Christian Höner zu Siederdissen, and Andrew John Gill, The HERMIT in the Stream: Fusing Stream Fusion's concatmap, Partial Evaluation and Program Manipulation (PEPM), ACM, 2014. [ DOI ]
[Gam09]
Peter Gammie, The worker/wrapper transformation, Archive of Formal Proofs (2009). [ http ]
[Gil96]
Andrew John Gill, Cheap deforestation for non-strict functional languages, Ph.D. thesis, University of Glasgow, 1996.
[GLP93]
Andrew John Gill, John Launchbury, and Simon Peyton Jones, A short cut to deforestation, Functional Programming Languages and Computer Architecture (FPCA), ACM, 1993. [ DOI ]
[GS99]
Jörgen Gustavsson and David Sands, A foundation for space-safe transformations of call-by-need programs, Higher Order Operational Techniques in Semantics (HOOTS), ENTCS, vol. 26, 1999. [ DOI ]
[GS01]
           , Possibilities and limitations of call-by-need space improvement, International Conference on Functional Programming (ICFP), ACM, 2001. [ DOI ]
[Haf09]
Florian Haftmann, Code generation from specifications in higher order logic, Ph.D. thesis, Technische Universität München, 2009.
[Haf10]
           , From higher-order logic to Haskell: There and back again, Partial Evaluation and Program Manipulation (PEPM), ACM, 2010. [ DOI ]
[HH14]
Jennifer Hackett and Graham Hutton, Worker/Wrapper/Makes It/Faster, International Conference on Functional Programming (ICFP), ACM, 2014. [ DOI ]
[HHM07]
Jurriaan Hage, Stefan Holdermans, and Arie Middelkoop, A generic usage analysis with subeffect qualifiers, International Conference on Functional Programming (ICFP), ACM, 2007. [ DOI ]
[HK13]
Brian Huffman and Ondřej Kunčar, Lifting and transfer: A modular design for quotients in Isabelle/HOL, Certified Programs and Proofs (CPP), LCNS, vol. 8307, Springer, 2013. [ DOI ]
[HL15]
Ralf Hinze and Andres Löh, lhs2tex: Preprocessor for typesetting Haskell sources with LaTeX, April 2015. [ http ]
[Huf12]
Brian Huffman, HOLCF '11: A definitional domain theory for verifying functional programs, Ph.D. thesis, Portland State University, 2012.
[JNR02]
Rajeev Joshi, Greg Nelson, and Keith Randall, Denali: A goal-directed superoptimizer, ACM, 2002. [ DOI ]
[KMNO14]
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens, CakeML: A verified implementation of ML, Principles of Programming Languages (POPL), ACM, 2014. [ DOI ]
[Lau93]
John Launchbury, A natural semantics for lazy evaluation, Principles of Programming Languages (POPL), ACM, 1993. [ DOI ]
[Ler06]
Xavier Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, Principles of Programming Languages (POPL), ACM, 2006. [ DOI ]
[Ler12]
           , Mechanized semantics for compiler verification, Asian Symposium on Programming Languages and Systems (APLAS), LNCS, vol. 7705, Springer, 2012, Invited talk. [ DOI ]
[LH14]
Andreas Lochbihler and Johannes Hölzl, Recursive functions on lazy lists via domains and topologies, Interactive Theorem Proving (ITP), LNCS (LNAI), vol. 8558, Springer, 2014. [ DOI ]
[Loc10]
Andreas Lochbihler, Verifying a compiler for Java Threads, European Symposium on Programming (ESOP), LNCS, vol. 6012, Springer, 2010. [ DOI ]
[Mar10]
Simon Marlow (ed.), Haskell 2010 language report, 2010.
[MDHS09]
Todd Mytkowicz, Amer Diwan, Matthias Hauswirth, and Peter F. Sweeney, Producing wrong data without doing anything obviously wrong!, Architectural Support for Programming Languages and Operating Systems (ASPLOS), ACM, 2009. [ DOI ]
[Mid12]
Jan Midtgaard, Control-flow analysis of functional programs, ACM Computing Surveys (CSUR) 44 (2012), no. 3. [ DOI ]
[MO03]
Yasuhiko Minamide and Koji Okuma, Verifying CPS transformations in Isabelle/HOL, Mechanized Reasoning About Languages with Variable Binding (MERLIN), ACM, 2003. [ DOI ]
[MP06]
Simon Marlow and Simon Peyton Jones, Making a fast curry: push/enter vs. eval/apply for higher-order languages, Journal of Functional Programming 16 (2006), no. 4-5. [ DOI ]
[MP12]
           , The Glasgow Haskell Compiler, The Architecture of Open Source Applications, Volume II (Amy Brown and Greg Wilson, eds.), Lulu, 2012.
[MS99]
Andrew K. Moran and David Sands, Improvement in a Lazy Context: An Operational Theory for Call-By-Need, Principles of Programming Languages (POPL), ACM, 1999. [ DOI ]
[Nak10]
Keiko Nakata, Denotational semantics for lazy initialization of letrec: black holes as exceptions rather than divergence, Fixed Points in Computer Science (FICS), 2010.
[NH09]
Keiko Nakata and Masahito Hasegawa, Small-step and big-step semantics for call-by-need, Journal of Functional Programming 19 (2009), no. 6. [ DOI ]
[Nip02]
Tobias Nipkow, Structured proofs in Isar/HOL, Types for Proofs and Programs (TYPES), LNCS, vol. 2646, Springer, 2002. [ DOI ]
[NPW02]
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel, Isabelle/HOL -- a proof assistant for higher-order logic, LNCS, vol. 2283, Springer, 2002. [ DOI ]
[NS07]
Nicholas Nethercote and Julian Seward, Valgrind: A framework for heavyweight dynamic binary instrumentation, Programming Language Design and Implementation (PLDI), ACM, 2007. [ DOI ]
[O'S15]
Bryan O'Sullivan, criterion: Robust, reliable performance measurement and analysis, March 2015. [ http ]
[Par93]
Will Partain, The nofib benchmark suite of haskell programs, Functional Programming 1992, Workshops in Computing, Springer, 1993. [ DOI ]
[PB10]
Maciej Pirog and Dariusz Biernacki, A systematic derivation of the stg machine verified in coq, Haskell Symposium, ACM, 2010. [ DOI ]
[Pey92]
Simon Peyton Jones, Implementing lazy functional languages on stock hardware: The spineless tagless G-machine, Journal of Functional Programming 2 (1992), no. 2. [ DOI ]
[Pit03]
Andrew M. Pitts, Nominal logic, a first order theory of names and binding, vol. 186, Information and Computation, no. 2, Elsevier, 2003. [ DOI ]
[PM02]
Simon Peyton Jones and Simon Marlow, Secrets of the glasgow haskell compiler inliner, Journal of Functional Programming 12 (2002), no. 5. [ DOI ]
[PTH01]
Simon Peyton Jones, Andrew Tolmach, and Tony Hoare, Playing by the rules: rewriting as a practical optimisation technique in GHC, Haskell Workshop, 2001.
[PVWW06]
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn, Simple unification-based type inference for GADTs, International Conference on Functional Programming (ICFP), ACM, 2006. [ DOI ]
[RDPJ10]
Norman Ramsey, João Dias, and Simon Peyton Jones, Hoopl: A modular, reusable library for dataflow analysis and transformation, Haskell Symposium, ACM, 2010. [ DOI ]
[rep03]
Haskell 98 language and libraries -- the revised report, 2003.
[RH15]
Tobias Rittweiler and Florian Haftmann, Haskabelle -- converting Haskell source files to Isabelle/HOL theories, 2015. [ .html ]
[San92]
David Sands, Operational theories of improvement in functional languages (extended abstract), Glasgow Workshop on Functional Programming 1991, Workshops in Computing, Springer, 1992. [ DOI ]
[SCPD07]
Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly, System F with type equality coercions, Types in Languages Design and Implementation (TLDI), ACM, 2007. [ DOI ]
[Ses97]
Peter Sestoft, Deriving a lazy abstract machine, Journal of Functional Programming 7 (1997), no. 03. [ DOI ]
[SHO10]
Lidia Sánchez-Gil, Mercedes Hidalgo-Herrero, and Yolanda Ortega-Mallén, An operational semantics for distributed lazy evaluation, Trends in Functional Programming (TFP) 2009, Intellect, 2010.
[SHO11]
           , Relating function spaces to resourced function spaces, Symposium on Applied Computing (SAC), ACM, 2011. [ DOI ]
[SHO12]
           , A locally nameless representation for a natural semantics for lazy evaluation, Theoretical Aspects of Computing (ICTAC), LNCS, vol. 7521, Springer, 2012. [ DOI ]
[SHO14]
           , Launchbury’s semantics revisited: On the equivalence of context-heap semantics (work in progress), XIV Jornadas sobre Programación y Lenguajes (2014).
[SHO15]
           , The role of indirections in lazy natural semantics, Perspectives of System Informatics (PSI) 2014, LNCS, vol. 8974, Springer, 2015. [ DOI ]
[SPCS08]
Tom Schrijvers, Simon Peyton Jones, Manuel M. T. Chakravarty, and Martin Sulzmann, Type checking with open type functions, International Conference on Functional Programming (ICFP), ACM, 2008. [ DOI ]
[Sve02]
Josef Svenningsson, Shortcut fusion for accumulating parameters & zip-like functions, International Conference on Functional Programming (ICFP), ACM, 2002. [ DOI ]
[SVP14]
Ilya Sergey, Dimitrios Vytiniotis, and Simon Peyton Jones, Modular, Higher-order Cardinality Analysis in Theory and Practice, Principles of Programming Languages (POPL), ACM, 2014. [ DOI ]
[Tak14]
Akio Takano, Worker-wrapper fusion, 2014, Prototype. [ http ]
[Tia06]
Ye Henry Tian, Mechanically verifying correctness of CPS compilation, Computing: The Australasian Theory Symposium (CATS), CRPIT, vol. 51, ACS, 2006, pp. 41--51.
[UK12]
Christian Urban and Cezary Kaliszyk, General bindings and alpha-equivalence in nominal Isabelle, Logical Methods in Computer Science 8 (2012), no. 2. [ DOI ]
[UT05]
Christian Urban and Christine Tasson, Nominal techniques in Isabelle/HOL, Automated Deduction – CADE-20, LNCS, vol. 3632, Springer, 2005. [ DOI ]
[VSJ+14]
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton Jones, Refinement types for Haskell, Iternational conference on Functional programming (ICFP), ACM, 2014. [ DOI ]
[WVPZ11]
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic, Generative type abstraction and type-level computation, Principles of Programming Languages (POPL), ACM, 2011. [ DOI ]
[XP05]
Dana N. Xu and Simon Peyton Jones, Arity analysis, 2005, Working notes.
[ZNMZ13]
Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic, Formal verification of SSA-based optimizations for LLVM, ACM, 2013. [ DOI ]