inproceedings: * author * title * booktitle (ausgeschrieben und abkürzung, Jahr wenn anders als die Veröffentlichung) * publisher oder series * ggf. volume/number/issue * year * doi article: * author * title * journal * volume, number * year * doi @inproceedings{launchbury, author = {John Launchbury}, title = {A Natural Semantics for Lazy Evaluation}, booktitle = {Principles of Programming Languages (POPL)}, year = {1993}, doi = {10.1145/158511.158618}, publisher = {ACM}, } bibsource = {DBLP, http://dblp.uni-trier.de} pages = {144-154}, @article{nakata, author = {Keiko Nakata and Masahito Hasegawa}, title = {Small-step and big-step semantics for call-by-need}, journal = {Journal of Functional Programming}, volume = {19}, number = {6}, year = {2009}, doi = {10.1017/S0956796809990219}, } pages = {699-722}, @article{nakata_extended, author = {Keiko Nakata and Masahito Hasegawa}, title = {Small-step and big-step semantics for call-by-need}, journal = {CoRR}, volume = {abs/0907.4640}, year = {2009}, } @inproceedings{nakata_blackhole, author = {Keiko Nakata}, title = {Denotational semantics for lazy initialization of letrec: black holes as exceptions rather than divergence}, booktitle = {Fixed Points in Computer Science (FICS)}, year = {2010}, } @inproceedings{functionspaces, author = {Lidia S{\'a}nchez{-}Gil and Mercedes Hidalgo{-}Herrero and Yolanda Ortega{-}Mall{\'e}n}, title = {Relating function spaces to resourced function spaces}, booktitle = {{S}ymposium on Applied Computing (SAC)}, publisher = {ACM}, year = {2011}, doi = {10.1145/1982185.1982469}, } pages = {1301-1308}, @inproceedings{nameless, author = {Lidia S{\'a}nchez{-}Gil and Mercedes Hidalgo{-}Herrero and Yolanda Ortega{-}Mall{\'e}n}, title = {A Locally Nameless Representation for a Natural Semantics for Lazy Evaluation}, booktitle = {Theoretical Aspects of Computing (ICTAC)}, year = {2012}, series = {LNCS}, volume = {7521}, publisher = {Springer}, doi = {10.1007/978-3-642-32943-2_8}, } pages = {105-119}, @inproceedings{distributed, author = {Lidia S{\'a}nchez{-}Gil and Mercedes Hidalgo{-}Herrero and Yolanda Ortega{-}Mall{\'e}n}, title = {An Operational Semantics for Distributed Lazy Evaluation}, booktitle = {Trends in Functional Programming (TFP) 2009}, publisher = {Intellect}, year = {2010}, } pages = {65-80}, @article{sanchezlaunchbury, title={Launchbury’s semantics revisited: On the equivalence of context-heap semantics (Work in progress)}, author = {Lidia S{\'a}nchez{-}Gil and Mercedes Hidalgo{-}Herrero and Yolanda Ortega{-}Mall{\'e}n}, journal={XIV Jornadas sobre Programaci{\'o}n y Lenguajes}, year={2014}, } pages={203-217}, @inproceedings{nominal, author = "Andrew M. Pitts", title = "Nominal logic, a first order theory of names and binding", series = "Information and Computation", volume = "186", number = "2", publisher = "Elsevier", year = "2003", doi = {10.1016/S0890-5401(03)00138-X}, } booktitle = "Theoretical Aspects of Computer Software (TACS) 2001", url = "http://www.sciencedirect.com/science/article/pii/S089054010300138X", pages = "165 - 193", issn = "0890-5401", @inproceedings{nominal_in_isabelle, author={Urban, Christian and Tasson, Christine}, title={Nominal Techniques in {Isabelle/HOL}}, booktitle={Automated Deduction – CADE-20}, series={LNCS}, volume={3632}, publisher={Springer}, year={2005}, doi={10.1007/11532231_4}, } pages={38-53}, @article{nominal2, author = {Christian Urban and Cezary Kaliszyk}, title = {General Bindings and Alpha-Equivalence in Nominal {Isabelle}}, journal = {Logical Methods in Computer Science}, volume = {8}, number = {2}, year = {2012}, doi = {10.2168/LMCS-8(2:14)2012}, } @techreport{mixed, author = {Eekelen, Marko van and Mol, Maarten de}, title = {Mixed lazy/strict graph semantics}, year = {2004}, month = {January}, number = {NIII-R0402}, institution = {Radboud University Nijmegen}, } @InProceedings{parallel, author = {Baker{-}Finch, Clem and King, David and Trinder, Phil}, title = {An Operational Semantics for Parallel Lazy Evaluation}, booktitle = {International Conference on Functional Programming (ICFP)}, publisher = {ACM}, year = {2000}, doi = {10.1145/351240.351256}, } @techreport{parallel-tr, author="Clem Baker{-}Finch and David King and Jon Hall and Phil Trinder", title="An Operational Semantics for Parallel Call-by-Need", institution="Faculty of Mathematics and Computing, The Open University", year=1999, number="99/1" } @article{sestoft, author = {Peter Sestoft}, title = {Deriving a lazy abstract machine}, journal = {Journal of Functional Programming}, volume = {7}, number = {03}, year = {1997}, doi = {10.1017/S0956796897002712}, } month = {4}, pages = {231--264}, @incollection{abramsky, author = {Samson Abramsky}, title = {The lazy lambda calculus}, editor = {Turner, David A.}, booktitle = {Research topics in functional programming}, year = {1990}, publisher = {Addison-Wesley}, chapter = 4, } pages = {65--116}, @article{launchbury-isa, author = {Joachim Breitner}, title = {The Correctness of {Launchbury}'s Natural Semantics for Lazy Evaluation}, journal = {Archive of Formal Proofs}, month = jan, year = 2013, url = {http://afp.sf.net/entries/Launchbury.shtml}, } ISSN = {2150-914x}, @inproceedings{indirections, author = {Lidia S{\'a}nchez{-}Gil and Mercedes Hidalgo{-}Herrero and Yolanda Ortega{-}Mall{\'e}n}, title = {The role of indirections in lazy natural semantics}, booktitle = {Perspectives of System Informatics (PSI) 2014}, series = {LNCS}, volume = {8974}, publisher = {Springer}, year = {2015}, doi = {10.1007/978-3-662-46823-4_24}, } @article{locales, author={Ballarin, Clemens}, title={Locales: A Module System for Mathematical Theories}, journal={Journal of Automated Reasoning}, volume={52}, number={2}, year={2014}, doi={10.1007/s10817-013-9284-7}, } publisher={Springer}, keywords={Theorem prover; Module system; Theory hierarchy; Theory interpretation; Isabelle}, language={English} pages={123-153}, url={http://dx.doi.org/10.1007/s10817-013-9284-7}, issn={0168-7433}, @article{arity-afp, author = {Joachim Breitner}, title = {{The Safety of Call Arity}}, journal = {Archive of Formal Proofs}, month = feb, year = 2015, url = {http://afp.sf.net/entries/Call_Arity.shtml}, } ISSN = {2150-914x}, @inproceedings{tfp, author = {Joachim Breitner}, title = {{Call Arity}}, booktitle = {Trends in Functional Programming (TFP) 2014}, series = {LNCS}, volume = {8843}, publisher = {Springer}, year = {2015}, doi = {10.1007/978-3-319-14675-1_3}, } pages = {34-50}, @misc{core, author = {Richard Eisenberg}, title = {{System FC, as implemented in GHC}}, url = {https://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf}, version = {414e20b}, urldate = {2015-04-24}, year = {2015}, } @article{inlinersecrets, author = {{Peyton Jones}, Simon and Marlow\thesimons, Simon}, title = {Secrets of the Glasgow Haskell Compiler Inliner}, journal = {Journal of Functional Programming}, volume = {12}, number = {5}, year = {2002}, doi = {10.1017/S0956796802004331}, } acmid = {968422}, publisher = {Cambridge University Press}, address = {New York, NY, USA}, issn = {0956-7968}, numpages = {42}, url = {http://dx.doi.org/10.1017/S0956796802004331}, month = jul, issue_date = {July 2002}, pages = {393--434}, @incollection{aos, author = {Marlow, Simon and {Peyton Jones}\thesimons, Simon}, title = {The {G}lasgow {H}askell {C}ompiler}, editor = {Amy Brown and Greg Wilson}, booktitle = {The Architecture of Open Source Applications, Volume II}, chapter = {5}, year = {2012}, publisher = {Lulu} } url = {http://www.aosabook.org/en/ghc.html}, @inproceedings{gadts, author = {{Peyton Jones}, Simon and Vytiniotis, Dimitrios and Weirich, Stephanie and Washburn, Geoffrey}, title = {Simple Unification-based Type Inference for {GADTs}}, booktitle = {International Conference on Functional Programming (ICFP)}, doi = {10.1145/1159803.1159811}, publisher = {ACM}, year = {2006}, } @inproceedings{typefamilies, author = {Schrijvers, Tom and {Peyton Jones}, Simon and Chakravarty, Manuel M. T. and Sulzmann, Martin}, title = {Type Checking with Open Type Functions}, booktitle = {International Conference on Functional Programming (ICFP)}, publisher = {ACM}, year = {2008}, doi = {10.1145/1411204.1411215}, } pages = {51--62}, @MISC{arityanalysis, author = {Dana N. Xu and Simon {Peyton Jones}}, title = {Arity Analysis}, note = {Working notes}, year = {2005} } @inproceedings{demandanalysis, author = {Sergey, Ilya and Vytiniotis, Dimitrios and {Peyton Jones}, Simon}, title = {{Modular, Higher-order Cardinality Analysis in Theory and Practice}}, booktitle = {Principles of Programming Languages (POPL)}, publisher = {ACM}, year = {2014}, doi = {10.1145/2535838.2535861}, } @article{fastcurry, author = {Marlow, Simon and {Peyton Jones}\thesimons, Simon}, title = {Making a fast curry: push/enter vs. eval/apply for higher-order languages}, journal = {Journal of Functional Programming}, volume = {16}, number = {4-5}, year = {2006}, doi = {10.1017/S0956796806005995}, } pages = {415-449}, @misc{ww-fusion, author = {Akio Takano}, title = {Worker-Wrapper Fusion}, note = {Prototype}, url = {https://github.com/takano-akio/ww-fusion}, urldate = {2014-02-02}, year = {2014}, } @phdthesis{gill, title={Cheap deforestation for non-strict functional languages}, author={Gill, Andrew John}, year={1996}, school={University of Glasgow} } @inproceedings{deforestation, author = {Gill, Andrew John and Launchbury, John and {Peyton Jones}, Simon}, title = {A Short Cut to Deforestation}, booktitle = {Functional Programming Languages and Computer Architecture (FPCA)}, publisher = {ACM}, year = {1993}, doi = {10.1145/165180.165214}, } address = {New York, NY, USA}, isbn = {0-89791-595-X}, location = {Copenhagen, Denmark}, numpages = {10}, pages = {223--232}, @inproceedings{rewriterules, title={Playing by the rules: rewriting as a practical optimisation technique in {GHC}}, author={{Peyton Jones}, Simon and Tolmach, Andrew and Hoare, Tony}, booktitle={Haskell Workshop}, year={2001} } pages={203--233}, @inproceedings{nofib, author = {Will Partain}, title = {The nofib Benchmark Suite of Haskell Programs}, booktitle = {Functional Programming 1992}, series = {Workshops in Computing}, publisher = {Springer}, year = {1993}, doi = {10.1007/978-1-4471-3215-8_17}, } pages = {195-202}, crossref = {DBLP:conf/fp/1992}, bibsource = {DBLP, http://dblp.uni-trier.de} @phdthesis{practicalfusion, title={Stream Fusion: Practical shortcut fusion for coinductive sequence types}, author={Coutts, Duncan}, year={2010}, school={University of Oxford} } @inproceedings{hermit, author = {Farmer, Andrew and {Höner zu Siederdissen}, Christian and Gill, Andrew John}, title = {The {HERMIT} in the {Stream}: Fusing {Stream} {Fusion's} concatMap}, booktitle = {Partial Evaluation and Program Manipulation (PEPM)}, publisher = {ACM}, year = {2014}, doi = {10.1145/2543728.2543736}, } @inproceedings{unfoldr, author = {Svenningsson, Josef}, title = {Shortcut Fusion for Accumulating Parameters \& Zip-like Functions}, booktitle = {International Conference on Functional Programming (ICFP)}, publisher = {ACM}, year = {2002}, doi = {10.1145/581478.581491}, } @INPROCEEDINGS{streamfusion, author = {Duncan Coutts and Roman Leshchinskiy and Don Stewart}, title = {Stream Fusion. From Lists to Streams to Nothing at All}, booktitle = {International Conference on Functional Programming (ICFP)}, year = {2007}, publisher = {ACM}, doi = {10.1145/1291151.1291199}, } @inproceedings{hage, author = {Jurriaan Hage and Stefan Holdermans and Arie Middelkoop}, title = {A generic usage analysis with subeffect qualifiers}, booktitle = {International Conference on Functional Programming (ICFP)}, publisher = {ACM}, year = {2007}, doi = {10.1145/1291151.1291189}, } pages = {235--246}, url = {http://doi.acm.org/10.1145/1291151.1291189}, @phdthesis{lochbihler12thesis, title = {A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler}, year = {2012}, month = jul, author = {Andreas Lochbihler}, school = {KIT}, } doi = {10.5445/KSP/1000028867}, url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000028867}, @inproceedings{jinjathreadscompiler, author = {Andreas Lochbihler}, title = {Verifying a Compiler for {J}ava {T}hreads}, booktitle = {European Symposium on Programming (ESOP)}, series = {LNCS}, volume = {6012}, publisher = {Springer}, year = {2010}, doi = {10.1007/978-3-642-11957-6_23}, } month = mar, pages = {427--447}, editor = {A. D. Gordon}, @inproceedings{cpsisabelle, author = {Minamide, Yasuhiko and Okuma, Koji}, title = {Verifying {CPS} Transformations in {I}sabelle/{HOL}}, booktitle = {Mechanized Reasoning About Languages with Variable Binding (MERLIN)}, publisher = {ACM}, year = {2003}, doi = {10.1145/976571.976576}, } location = {Uppsala, Sweden}, numpages = {8}, acmid = {976576}, keywords = {correctness proofs, program transformation, theorem proving}, isbn = {1-58113-800-8}, url = {http://doi.acm.org/10.1145/976571.976576}, address = {New York, NY, USA}, booktitle = {Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning About Languages with Variable Binding}, @article{WorkerWrapper-AFP, author = {Peter Gammie}, title = {The Worker/Wrapper Transformation}, journal = {Archive of Formal Proofs}, month = oct, year = 2009, url = {http://afp.sf.net/entries/WorkerWrapper.shtml}, } ISSN = {2150-914x}, @inproceedings{cpstwelf, Author = {Tian, Ye Henry}, Title = {Mechanically Verifying Correctness of {CPS} Compilation}, BookTitle = {Computing: The Australasian Theory Symposium (CATS)}, Series= {CRPIT}, Publisher = {ACS}, Volume = {51}, Pages = {41-51}, Year = {2006} } Address= {Hobart, Australia}, Editor = {Gudmundsson, Joachim and Jay, Barry}, @incollection{cpscoq, author={Dargaye, Zaynah and Leroy, Xavier}, title={{Mechanized Verification of CPS Transformations}}, booktitle={Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)}, series={LNCS}, volume={4790}, publisher={Springer}, year={2007}, doi={10.1007/978-3-540-75560-9_17}, } language={English} pages={211-225}, editor={Dershowitz, Nachum and Voronkov, Andrei}, isbn={978-3-540-75558-6}, url={http://dx.doi.org/10.1007/978-3-540-75560-9_17}, @inproceedings{compcert, author = {Xavier Leroy}, title = {Mechanized Semantics for Compiler Verification}, note = {Invited talk}, booktitle = {Asian Symposium on Programming Languages and Systems (APLAS)}, series = {LNCS}, volume = 7705, publisher = {Springer}, year = {2012}, doi = {10.1007/978-3-642-35182-2_27}, } xtopic = {mechsem}, refereed = {no}, abstract = {The formal verification of compilers and related programming tools depends crucially on the availability of appropriate mechanized semantics for the source, intermediate and target languages. In this invited talk, I review various forms of operational semantics and their mechanization, based on my experience with the formal verification of the CompCert~C compiler.} pages = {386--388}, editor = {Ranjit Jhala and Atsushi Igarashi}, url = {http://gallium.inria.fr/~xleroy/publi/mechanized-semantics-aplas-cpp-2012.pdf}, @inproceedings{compcert2, author = {Xavier Leroy}, title = {Formal certification of a compiler back-end, or: programming a compiler with a proof assistant}, booktitle = {Principles of Programming Languages (POPL)}, year = 2006, publisher = {ACM}, doi = {10.1145/1111037.1111042}, } urllocal = {http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf}, pages = {42--54}, abstract = {This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.}, xtopic = {compcert} @inproceedings{ltamer, author = {Chlipala, Adam}, title = {A Verified Compiler for an Impure Functional Language}, booktitle = {Principles of Programming Languages (POPL)}, year = {2010}, publisher = {ACM}, doi = {10.1145/1706299.1706312}, } location = {Madrid, Spain}, pages = {93--106}, keywords = {compiler verification, interactive proof assistants}, numpages = {14}, acmid = {1706312}, isbn = {978-1-60558-479-9}, url = {http://doi.acm.org/10.1145/1706299.1706312}, address = {New York, NY, USA}, @phdthesis{holcf, author = {Brian Huffman}, title = {{HOLCF} '11: A Definitional Domain Theory for Verifying Functional Programs}, school = {Portland State University}, year = {2012} } @Book{isabelle, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {{I}sabelle/{HOL} -- A Proof Assistant for Higher-Order Logic}, series = {LNCS}, volume = 2283, publisher = {Springer}, year = 2002, doi = {10.1007/3-540-45949-9}, } @inproceedings{sands, author = {Jörgen Gustavsson and David Sands}, title = {Possibilities and Limitations of Call-by-Need Space Improvement}, booktitle = {International Conference on Functional Programming (ICFP)}, year = {2001}, publisher = {ACM}, doi = {10.1145/507635.507667}, } pages = {265--276}, crossref = {DBLP:conf/icfp/2001}, url = {http://doi.acm.org/10.1145/507635.507667}, timestamp = {Tue, 11 Jun 2013 13:50:18 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GustavssonS01}, bibsource = {dblp computer science bibliography, http://dblp.org} @inproceedings{Sands:Skye, author = {David Sands}, title = {Operational Theories of Improvement in Functional Languages (Extended Abstract)}, booktitle = {{G}lasgow Workshop on Functional Programming 1991}, series = {Workshops in Computing}, publisher = {Springer}, year = {1992}, doi={10.1007/978-1-4471-3196-0_24}, } pdf = {http://www.cse.chalmers.se/~dave/papers/Sands:Skye.pdf} pages = {298--311}, @inproceedings{Moran:Sands:Need, author = {Andrew K. Moran and David Sands}, title = {{Improvement in a Lazy Context: An Operational Theory for Call-By-Need}}, booktitle = {Principles of Programming Languages (POPL)}, year = {1999}, publisher = {ACM}, doi = {10.1145/292540.292547}, } pages = {43--56}, pdf = {http://www.cse.chalmers.se/~dave/papers/cbneed-theory.pdf} month = {January}, @inproceedings{wwmif, author = {Hackett, Jennifer and Hutton, Graham}, title = {{Worker/Wrapper/Makes It/Faster}}, booktitle = {International Conference on Functional Programming (ICFP)}, year = {2014}, publisher = {ACM}, doi = {10.1145/2628136.2628142}, } numpages = {13}, acmid = {2628142}, pages = {95--107}, url = {http://doi.acm.org/10.1145/2628136.2628142}, isbn = {978-1-4503-2873-9}, location = {Gothenburg, Sweden}, @inproceedings{Aspinall, author = "David Aspinall and Lennart Beringer and Alberto Momigliano", title = "Optimisation Validation", booktitle = "Compiler Optimisation Meets Compiler Verification (COCV) 2006", series = "ENTCS", volume = "176-3", year = "2007", doi = {10.1016/j.entcs.2006.06.017}, } pages = "37 - 59", url = "http://www.sciencedirect.com/science/article/pii/S1571066107005026", issn = "1571-0661", @inproceedings{cakeml, author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott}, title = {{CakeML}: A Verified Implementation of {ML}}, booktitle = {Principles of Programming Languages (POPL)}, publisher = {ACM}, year = {2014}, doi = {10.1145/2535838.2535841}, } pages = {179--191}, address = {New York, NY, USA}, keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking}, isbn = {978-1-4503-2544-8}, location = {San Diego, California, USA}, numpages = {13}, url = {http://doi.acm.org/10.1145/2535838.2535841}, acmid = {2535841}, @inproceedings{Sands:Foundation, author = {Jörgen Gustavsson and David Sands}, title = {A Foundation for Space-Safe Transformations of Call-by-Need Programs}, booktitle = {Higher Order Operational Techniques in Semantics (HOOTS)}, series = {ENTCS}, volume = {26}, year = {1999}, doi = {10.1016/S1571-0661(05)80284-1}, } pages = {69--86}, doi = {10.1016/S1571-0661(05)80284-1}, timestamp = {Mon, 20 Jun 2011 17:31:39 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/GustavssonS99}, bibsource = {dblp computer science bibliography, http://dblp.org} @article{fullabstraction, author = "Samson Abramsky and Chih-Hao Luke Ong", title = "Full Abstraction in the Lazy Lambda Calculus", journal = "Information and Computation", volume = "105", number = "2", year = "1993", doi = "10.1006/inco.1993.1044", } issn = "0890-5401", url = "http://www.sciencedirect.com/science/article/pii/S0890540183710448", note = "", pages = "159 - 267", @inproceedings{wrong-data, author = {Mytkowicz, Todd and Diwan, Amer and Hauswirth, Matthias and Sweeney, Peter F.}, title = {Producing Wrong Data Without Doing Anything Obviously Wrong!}, booktitle = {Architectural Support for Programming Languages and Operating Systems (ASPLOS)}, publisher = {ACM}, doi = {10.1145/1508284.1508275}, year = {2009}, } address = {New York, NY, USA}, numpages = {12}, pages = {265--276}, @inproceedings{stabilizer, author = {Curtsinger, Charlie and Berger, Emery D.}, title = {{STABILIZER:} Statistically Sound Performance Evaluation}, booktitle = {Architectural Support for Programming Languages and Operating Systems (ASPLOS)}, publisher = {ACM}, year = 2013, doi = {10.1145/2451116.2451141}, } @inproceedings{valgrind, author = {Nethercote, Nicholas and Seward, Julian}, title = {Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation}, booktitle = {Programming Language Design and Implementation (PLDI)}, publisher = {ACM}, year = {2007}, doi = {10.1145/1273442.1250746}, } @inproceedings{coinductive-filter, author = {Andreas Lochbihler and Johannes Hölzl}, title = {Recursive Functions on Lazy Lists via Domains and Topologies}, booktitle = {Interactive Theorem Proving (ITP)}, series = {LNCS (LNAI)}, volume = 8558, publisher = {Springer}, year = 2014, doi = {10.1007/978-3-319-08970-6_22}, } editor = {Gerwin Klein and Ruben Gamboa}, pages = {341--357}, @inproceedings{lifting, author={Huffman, Brian and Kunčar, Ondřej}, title={Lifting and Transfer: A Modular Design for Quotients in {I}sabelle/{HOL}}, booktitle={Certified Programs and Proofs (CPP)}, series={LCNS}, volume={8307}, publisher={Springer}, year={2013}, doi={10.1007/978-3-319-03545-1_9}, } url={http://dx.doi.org/10.1007/978-3-319-03545-1_9}, editor={Gonthier, Georges and Norrish, Michael}, language={English} pages={131-146}, % GET http://code.haskell.org/~thielema/bibtex/hackage.bib.gz|zcat|less @Misc{criterion, author = {Bryan {O'Sullivan}}, title = {{criterion: Robust, reliable performance measurement and analysis}}, url = {http://hackage.haskell.org/package/criterion-1.1.0.0}, year = {2015}, month = {March}, version = {1.1.0.0}, } keywords = {Haskell, Development, Performance, Testing, Benchmarking}, subtype = {program}, @Misc{lhs2tex, author = {Ralf Hinze and Andres Löh}, title = {{lhs2tex: Preprocessor for typesetting Haskell sources with LaTeX}}, url = {http://hackage.haskell.org/package/lhs2tex-1.19}, year = {2015}, month = {April}, version = {1.19}, } keywords = {Haskell, Development, Language}, subtype = {program}, @inproceedings{safe-coercions, author = {Breitner, Joachim and Eisenberg, Richard A. and {Peyton Jones}, Simon and Weirich, Stephanie}, title = {Safe Zero-cost Coercions for {H}askell}, booktitle = {International Conference on Functional Programming (ICFP)}, publisher = {ACM}, year = {2014}, doi = {10.1145/2628136.2628141}, } location = {Gothenburg, Sweden}, @inproceedings{generative-type-abstraction, author = {Stephanie Weirich and Dimitrios Vytiniotis and Simon {Peyton Jones} and Steve Zdancewic}, title = {Generative type abstraction and type-level computation}, booktitle = {Principles of Programming Languages (POPL)}, publisher = {ACM}, year = {2011}, doi = {10.1145/1926385.1926411}, } pages = {227-240}, @InProceedings{systemfc, Title = {System {F} with type equality coercions}, Author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and {Peyton Jones}, Simon and Donnelly, Kevin}, Booktitle = {Types in Languages Design and Implementation (TLDI)}, Year = {2007}, Publisher = {ACM}, doi = {10.1145/1190315.1190324}, } @periodical{report ,editor={Simon {Peyton Jones}} ,title={Haskell 98 Language and Libraries -- The Revised Report} ,series = {Journal of Functional Programming} ,volume = {13} ,number = {1} ,year=2003 } ,publisher={Cambridge University Press} ,address={Cambridge, England} @book{report2010 ,editor={Simon {Marlow}} ,title={Haskell 2010 Language Report} ,year=2010 } @article{stg, author = {Simon {Peyton Jones}}, title = {Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless {G}-Machine}, journal = {Journal of Functional Programming}, volume = {2}, number = {2}, year = {1992}, doi = {10.1017/S0956796800000319}, } pages = {127--202}, @Manual{coq, title = {The {C}oq proof assistant reference manual}, author = {The {Coq development team}}, organization = {LogiCal Project}, note = {Version 8.0}, year = {2004}, url = "http://coq.inria.fr" } @inproceedings{isar, author = {Tobias Nipkow}, title = {Structured Proofs in {Isar/HOL}}, booktitle = {Types for Proofs and Programs (TYPES)}, series = {LNCS}, volume = {2646}, publisher = {Springer}, year = {2002}, doi = {10.1007/3-540-39185-1_15}, } timestamp = {Tue, 05 Jul 2011 11:09:27 +0200}, url = {http://dx.doi.org/10.1007/3-540-39185-1_15}, pages = {259--278}, @inproceedings{call-arity-safe, author = {Joachim Breitner}, title = {Formally proving a compiler transformation safe}, booktitle = {Haskell Symposium}, publisher = {{ACM}}, year = {2015}, doi = {10.1145/2804302.2804312}, } pages = {35--46}, @misc{launchbury-adequacy-preprint, author = {Joachim Breitner}, title = {{The Adequacy of Launchbury's Natural Semantics for Lazy Evaluation}}, year = {2015}, url = {http://joachim-breitner.de/publications/LaunchburyAdequacy-preprint.pdf}, note = {preprint, submitted to the Journal of Functional Programming} } @article{bird, author = {Bird, Richard Simpson}, title = {Algebraic Identities for Program Calculation}, journal = {Computer Journal}, volume = {32}, number = {2}, year = {1989}, doi = {10.1093/comjnl/32.2.122}, } pages = {122-126}, @inproceedings{haskell-formalisation, author = {Haftmann, Florian}, title = {From Higher-order Logic to {H}askell: There and Back Again}, booktitle = {Partial Evaluation and Program Manipulation (PEPM)}, publisher = {ACM}, year = {2010}, doi = {10.1145/1706356.1706385}, } address = {New York, NY, USA}, acmid = {1706385}, isbn = {978-1-60558-727-1}, location = {Madrid, Spain}, pages = {155--158}, numpages = {4}, @phdthesis{codegen, title={Code Generation from Specifications in Higher Order Logic}, author={Haftmann, Florian}, year={2009}, school={Technische Universität München} } @inproceedings{refinement-types, author = {Niki Vazou and Eric L. Seidel and Ranjit Jhala and Dimitrios Vytiniotis and Simon {Peyton Jones}}, title = {Refinement types for {H}askell}, booktitle = {Iternational conference on Functional programming (ICFP)}, publisher = {ACM}, year = {2014}, doi = {10.1145/2628136.2628161}, } pages = {269--282}, @inproceedings{hart, author = {Joachim Breitner and Brian Huffman and Neil Mitchell and Christian Sternagel}, title = {Certified {HLints} with {Isabelle/HOLCF-Prelude}}, booktitle = "Haskell and Rewriting Techniques (HART)", eprinttype = {arXiv}, eprint = {1306.1340}, year = {2013}, } @misc{haskabelle, title = {Haskabelle -- converting {H}askell source files to {Isabelle/HOL} theories}, author = {Tobias Rittweiler and Florian Haftmann}, url = {http://isabelle.in.tum.de/haskabelle.html}, year = {2015}, } @article{functional-cfg, author = {Midtgaard, Jan}, title = {Control-flow Analysis of Functional Programs}, journal = {ACM Computing Surveys (CSUR)}, volume = {44}, number = {3}, month = jun, year = {2012}, doi = {10.1145/2187671.2187672}, } @inproceedings{hoopl, author = {Ramsey, Norman and Dias, Jo\~{a}o and Peyton Jones, Simon}, title = {Hoopl: A Modular, Reusable Library for Dataflow Analysis and Transformation}, booktitle = {Haskell Symposium}, publisher = {ACM}, year = {2010}, doi = {10.1145/1863523.1863539}, } @inproceedings{biernacki, author = {Pirog, Maciej and Biernacki, Dariusz}, title = {A Systematic Derivation of the STG Machine Verified in Coq}, booktitle = {Haskell Symposium}, publisher = {ACM}, year = {2010}, doi = {10.1145/1863523.1863528}, } @inproceedings{vellvm, author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, Steve}, title = {Formal Verification of {SSA}-based Optimizations for {LLVM}}, bootktitle = {Programming Language Design and Implementation (PLDI)}, year = {2013}, publisher = {ACM}, doi = {10.1145/2491956.2462164}, } @inproceedings{bansal, author = {Bansal, Sorav and Aiken, Alex}, title = {Automatic Generation of Peephole Superoptimizers}, booktitle = {Architectural Support for Programming Languages and Operating Systems (ASPLOS)}, year = {2006}, doi = {10.1145/1168857.1168906}, publisher = {ACM}, } @Inbook{optgen, author="Buchwald, Sebastian", title="Optgen: A Generator for Local Optimizations", bookTitle="Compiler Construction", year="2015", series={LCNS}, volume={9031}, publisher="Springer", doi="10.1007/978-3-662-46663-6_9", } @inproceedings{denali, author = {Joshi, Rajeev and Nelson, Greg and Randall, Keith}, title = {Denali: A Goal-directed Superoptimizer}, bootktitle = {Programming Language Design and Implementation (PLDI)}, year = {2002}, doi = {10.1145/512529.512566}, publisher = {ACM}, }