@inproceedings{launchbury,
  author    = {John Launchbury},
  title     = {A Natural Semantics for Lazy Evaluation},
  booktitle = {POPL '93},
  year      = {1993},
  pages     = {144-154},
  ee        = {http://doi.acm.org/10.1145/158511.158618},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@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},
  pages     = {699-722},
  doi       = {10.1017/S0956796809990219},
}

@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: black holes as exceptions rather than nontermination},
    year = {2010},
    booktitle = {FICS},
}

@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 = {PSI},
  year      = {2014},
}

@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 = {SAC},
  year      = {2011},
  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 = {ICTAC},
  year      = {2012},
  pages     = {105-119},
  doi       = {10.1007/978-3-642-32943-2_8},
}

@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},
  volume    = {10},
  pages     = {65-80},
  year      = {2010},
  publisher = {Intellect},
}


@phdthesis{holcf,
  author = {Brian Huffman},
  title = {{HOLCF} '11: A Definitional Domain Theory for Verifying Functional Programs},
  school = {Portland State University},
  year = {2012}
}

@article{nominal,
  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},
}

@misc{mixed,
  author    = {Marko van Eekelen and Maarten de Mol}, 
  title     = {Mixed lazy/strict graph semantics},
  year      = {2004},
  month     = {January},
  note      = {Technical Report NIII-R0402, Radboud University Nijmegen},
  }

@article{parallel,
 author = {Baker-Finch, Clem and King, David J. and Trinder, Phil},
 title = {An operational semantics for parallel lazy evaluation},
 journal = {ICFP},
 volume = {35},
 number = {9},
 month = sep,
 year = {2000},
 pages = {162--173},
 doi = {10.1145/357766.351256},
 acmid = {351256},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@article{sestoft,
	author = {Peter Sestoft},
	title = {Deriving a lazy abstract machine},
	journal = {Journal of Functional Programming},
	volume = {7},
	issue = {03},
	month = {4},
	year = {1997},
	pages = {231--264},
	doi = {10.1017/S0956796897002712},
}

@incollection{abramsky,
 author = {Samson Abramsky},
 title = {The lazy lambda calculus},
 booktitle = {Research topics in functional programming},
 year = {1990},
 pages = {65--116},
}

@article{fullabstraction,
title = "Full Abstraction in the Lazy Lambda Calculus ",
journal = "Information and Computation ",
volume = "105",
number = "2",
pages = "159 - 267",
year = "1993",
note = "",
issn = "0890-5401",
doi = "http://dx.doi.org/10.1006/inco.1993.1044",
url = "http://www.sciencedirect.com/science/article/pii/S0890540183710448",
author = "Samson Abramsky and Chih-Hao Luke Ong"
}

@article{breitner2013,
  author  = {Joachim Breitner},
  title   = {The Correctness of Launchbury's Natural Semantics for Lazy Evaluation},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2013,
  note    = {\url{http://afp.sf.net/entries/Launchbury.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@inproceedings{tfp,
  title = {{Call Arity}},
  booktitle = {TFP'14},
  year = {2015},
  publisher = {Springer},
  pages = {34-50},
  author = {Joachim Breitner},
  series = {LNCS},
  volume = {8843},
  doi = {10.1007/978-3-319-14675-1_3},
}


@inproceedings{icfp15,
  author  = {Joachim Breitner},
  title = {{Formally proving a compiler transformation safe}},
  booktitle = {ICFP'15},
  year = {2015},
  publisher = {ACM},
  note = {submitted},
}

@article{callarity-afp,
  author  = {Joachim Breitner},
  title   = {{The Safety of Call Arity}},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2015,
  note    = {\url{http://afp.sf.net/entries/Call_Arity.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}