@article(ariola:97,
 author       = {Z. M. Ariola and M. Felleisen},
 year         = {1997},
 title        = {The Call-By-Need lambda Calculus},
 journal      = {JFP},
 volume       = {7},
 number       = {3},
 pages        = {265--301},
)
@inproceedings(ariola:95,
 author       = {Z. M. Ariola and M. Felleisen and J. Maraist and M. Odersky and P. Wadler},
 year         = {1995},
 title        = {A call-by-need lambda calculus},
 booktitle    = {{POPL} 1995},
 publisher    = {ACM},
 pages        = {233--246},
 doi          = {10.1145/199448.199507},
)
@book(Baader:1998:TR:280474,
 author       = {F. Baader and T. Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139172752},
)
@inproceedings(DBLP:conf/rta/FuhsGPSF09,
 author       = {C. Fuhs and J. Giesl and M.Pl{\"{u}}cker and Schneider{-}Kamp, P. and S. Falke},
 year         = {2009},
 title        = {Proving Termination of Integer Term Rewriting},
 booktitle    = {{RTA} 2009},
 series       = {LNCS},
 volume       = {5595},
 publisher    = {Springer},
 pages        = {32--47},
 doi          = {10.1007/978-3-642-02348-4\_3},
)
@inproceedings(FBEFFOPSKSST:14,
 author       = {J. Giesl and M. Brockschmidt and F. Emmes and F. Frohn and C. Fuhs and C. Otto and M. Pl{\"{u}}cker and Schneider{-}Kamp, P. and T. Str{\"{o}}der and S. Swiderski and R. Thiemann},
 year         = {2014},
 title        = {Proving Termination of Programs Automatically with {AProVE}},
 booktitle    = {{IJCAR} 2014},
 series       = {LNCS},
 volume       = {8562},
 publisher    = {Springer},
 pages        = {184--191},
 doi          = {10.1007/978-3-319-08587-6\_13},
)
@inproceedings(Jez14,
 author       = {A. Jez},
 year         = {2014},
 title        = {Context Unification is in {PSPACE}},
 booktitle    = {ICALP 2014, Part II},
 series       = {LNCS},
 volume       = {8573},
 publisher    = {Springer},
 pages        = {244--255},
 doi          = {10.1007/978-3-662-43951-7\_21},
)
@inproceedings(machkasova-turbak:00,
 author       = {E. Machkasova and F. A. Turbak},
 year         = {2000},
 title        = {A Calculus for Link-Time Compilation},
 booktitle    = {{ESOP} 2000},
 series       = {LNCS},
 volume       = {1782},
 publisher    = {Springer},
 pages        = {260--274},
 doi          = {10.1007/3-540-46425-5\_17},
)
@book(milner:book,
 author       = {R. Milner},
 year         = {1999},
 title        = {Communicating and mobile systems - the Pi-calculus},
 publisher    = {Cambridge University Press},
)
@phdthesis(morris:68,
 author       = {J. H. Morris},
 year         = {1968},
 title        = {Lambda-Calculus Models of Programming Languages},
 school       = {MIT},
)
@article(plotkin:75,
 author       = {G. D. Plotkin},
 year         = {1975},
 title        = {Call-by-name, call-by-value, and the lambda-calculus},
 journal      = {Theoret. Comput. Sci.},
 volume       = {1},
 pages        = {125--159},
 doi          = {10.1016/0304-3975(75)90017-1},
)
@inproceedings(rau-sabel-schmidtschauss:12,
 author       = {C. Rau and D. Sabel and Schmidt-Schau{\ss}, M.},
 year         = {2012},
 title        = {Correctness of Program Transformations as a Termination Problem},
 booktitle    = {{IJCAR} 2012},
 series       = {LNCS},
 volume       = {7364},
 publisher    = {Springer},
 pages        = {462--476},
 doi          = {10.1007/978-3-642-31365-3\_36},
)
@inproceedings(sabel-17:ppdp17,
 author       = {D. Sabel},
 year         = {2017},
 title        = {Alpha-renaming of Higher-order Meta-expressions},
 booktitle    = {PPDP 2017},
 publisher    = {ACM},
 pages        = {151--162},
 doi          = {10.1145/3131851.3131866},
)
@inproceedings(sabel-unif:17,
 author       = {D. Sabel},
 year         = {2017},
 title        = {Matching of Meta-Expressions with Recursive Bindings},
 booktitle    = {Informal Proceedings of {UNIF} 2017},
 url          = {unif-workshop.github.io/UNIF2017/papers/UNIF_2017_paper_2.pdf},
)
@techreport(sabel:2017-match,
 author       = {D. Sabel},
 year         = {2017},
 title        = {Rewriting of Higher-Order Meta-Expressions with Recursive Bindings},
 type         = {Frankfurter Informatik-Berichte},
 number       = {2017-1},
 institution  = {Goethe-University Frankfurt},
 url          = {d-nb.info/1136368175/34},
)
@article(sabel-schmidt-schauss-MSCS:08,
 author       = {D. Sabel and Schmidt-Schau{\ss}, M.},
 year         = {2008},
 title        = {A Call-by-Need Lambda-Calculus with Locally Bottom-Avoiding Choice: Context Lemma and Correctness of Transformations},
 journal      = {Math. Structures Comput. Sci.},
 volume       = {18},
 number       = {03},
 pages        = {501--553},
 doi          = {10.1017/S0960129508006774},
)
@inproceedings(sabel-schmidt-schauss-PPDP:2011,
 author       = {D. Sabel and Schmidt-Schau{\ss}, M.},
 year         = {2011},
 title        = {A contextual semantics for concurrent Haskell with futures},
 booktitle    = {PPDP 2011},
 publisher    = {ACM},
 pages        = {101--112},
 doi          = {10.1145/2003476.2003492},
)
@article(schmidt-schauss-sabel-gencontext:10,
 author       = {Schmidt-Schau{\ss}, M. and D. Sabel},
 year         = {2010},
 title        = {On generic context lemmas for higher-order calculi with sharing},
 journal      = {Theoret. Comput. Sci.},
 volume       = {411},
 number       = {11-13},
 pages        = {1521 -- 1541},
 doi          = {10.1016/j.tcs.2009.12.001},
)
@inproceedings(schmidtschauss-sabel-PPDP:2016,
 author       = {Schmidt-Schau{\ss}, M. and D. Sabel},
 year         = {2016},
 title        = {Unification of Program Expressions with Recursive Bindings},
 booktitle    = {{PPDP} 2016},
 publisher    = {ACM},
 pages        = {160--173},
 doi          = {10.1145/2967973.2968603},
)
@inproceedings(schmidt-schauss-sabel-machkasova-rta:10,
 author       = {Schmidt-Schau{\ss}, M. and D. Sabel and E. Machkasova},
 year         = {2010},
 title        = {Simulation in the Call-by-Need Lambda-Calculus with letrec},
 booktitle    = {{RTA} 2010},
 series       = {LIPIcs},
 volume       = {6},
 publisher    = {Schloss Dagstuhl},
 pages        = {295--310},
 doi          = {10.4230/LIPIcs.RTA.2010.295},
)
@article(schmidt-schauss-schuetz-sabel:08,
 author       = {Schmidt-Schau{\ss}, M. and M. Sch\"utz and D. Sabel},
 year         = {2008},
 title        = {Safety of {N}\"ocker's Strictness Analysis},
 journal      = {JFP},
 volume       = {18},
 number       = {04},
 pages        = {503--551},
 doi          = {10.1017/S0956796807006624},
)
@inproceedings(DBLP:conf/tphol/ThiemannS09,
 author       = {R. Thiemann and C. Sternagel},
 year         = {2009},
 title        = {Certification of Termination Proofs Using CeTA},
 booktitle    = {{TPHOLs} 2009},
 series       = {LNCS},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {452--468},
 doi          = {10.1007/978-3-642-03359-9\_31},
)
@inproceedings(wells-plump-kamareddine:03,
 author       = {J. B. Wells and D. Plump and F. Kamareddine},
 year         = {2003},
 title        = {Diagrams for Meaning Preservation},
 booktitle    = {RTA 2003},
 series       = {LNCS},
 volume       = {2706},
 publisher    = {Springer},
 pages        = {88 --106},
 doi          = {10.1007/3-540-44881-0\_8},
)
@article(wright-felleisen:94,
 author       = {A. K. Wright and M. Felleisen},
 year         = {1994},
 title        = {A Syntactic Approach to Type Soundness},
 journal      = {Inf. Comput.},
 volume       = {115},
 number       = {1},
 pages        = {38--94},
 doi          = {10.1006/inco.1994.1093},
)