Z. M. Ariola & M. Felleisen (1997):
The Call-By-Need lambda Calculus.
JFP 7(3),
pp. 265–301.
Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky & P. Wadler (1995):
A call-by-need lambda calculus.
In: POPL 1995.
ACM,
pp. 233–246,
doi:10.1145/199448.199507.
F. Baader & T. Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press,
doi:10.1017/CBO9781139172752.
C. Fuhs, J. Giesl, M.Plücker, P. Schneider-Kamp & S. Falke (2009):
Proving Termination of Integer Term Rewriting.
In: RTA 2009,
LNCS 5595.
Springer,
pp. 32–47,
doi:10.1007/978-3-642-02348-4_3.
J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski & R. Thiemann (2014):
Proving Termination of Programs Automatically with AProVE.
In: IJCAR 2014,
LNCS 8562.
Springer,
pp. 184–191,
doi:10.1007/978-3-319-08587-6_13.
A. Jez (2014):
Context Unification is in PSPACE.
In: ICALP 2014, Part II,
LNCS 8573.
Springer,
pp. 244–255,
doi:10.1007/978-3-662-43951-7_21.
E. Machkasova & F. A. Turbak (2000):
A Calculus for Link-Time Compilation.
In: ESOP 2000,
LNCS 1782.
Springer,
pp. 260–274,
doi:10.1007/3-540-46425-5_17.
R. Milner (1999):
Communicating and mobile systems - the Pi-calculus.
Cambridge University Press.
J. H. Morris (1968):
Lambda-Calculus Models of Programming Languages.
MIT.
G. D. Plotkin (1975):
Call-by-name, call-by-value, and the lambda-calculus.
Theoret. Comput. Sci. 1,
pp. 125–159,
doi:10.1016/0304-3975(75)90017-1.
C. Rau, D. Sabel & M. Schmidt-Schauß (2012):
Correctness of Program Transformations as a Termination Problem.
In: IJCAR 2012,
LNCS 7364.
Springer,
pp. 462–476,
doi:10.1007/978-3-642-31365-3_36.
D. Sabel (2017):
Alpha-renaming of Higher-order Meta-expressions.
In: PPDP 2017.
ACM,
pp. 151–162,
doi:10.1145/3131851.3131866.
D. Sabel (2017):
Rewriting of Higher-Order Meta-Expressions with Recursive Bindings.
Frankfurter Informatik-Berichte 2017-1.
Goethe-University Frankfurt.
Available at d-nb.info/1136368175/34.
D. Sabel & M. Schmidt-Schauß (2008):
A Call-by-Need Lambda-Calculus with Locally Bottom-Avoiding Choice: Context Lemma and Correctness of Transformations.
Math. Structures Comput. Sci. 18(03),
pp. 501–553,
doi:10.1017/S0960129508006774.
D. Sabel & M. Schmidt-Schauß (2011):
A contextual semantics for concurrent Haskell with futures.
In: PPDP 2011.
ACM,
pp. 101–112,
doi:10.1145/2003476.2003492.
M. Schmidt-Schauß & D. Sabel (2010):
On generic context lemmas for higher-order calculi with sharing.
Theoret. Comput. Sci. 411(11-13),
pp. 1521 – 1541,
doi:10.1016/j.tcs.2009.12.001.
M. Schmidt-Schauß & D. Sabel (2016):
Unification of Program Expressions with Recursive Bindings.
In: PPDP 2016.
ACM,
pp. 160–173,
doi:10.1145/2967973.2968603.
M. Schmidt-Schauß, D. Sabel & E. Machkasova (2010):
Simulation in the Call-by-Need Lambda-Calculus with letrec.
In: RTA 2010,
LIPIcs 6.
Schloss Dagstuhl,
pp. 295–310,
doi:10.4230/LIPIcs.RTA.2010.295.
M. Schmidt-Schauß, M. Schütz & D. Sabel (2008):
Safety of Nöcker's Strictness Analysis.
JFP 18(04),
pp. 503–551,
doi:10.1017/S0956796807006624.
R. Thiemann & C. Sternagel (2009):
Certification of Termination Proofs Using CeTA.
In: TPHOLs 2009,
LNCS 5674.
Springer,
pp. 452–468,
doi:10.1007/978-3-642-03359-9_31.
J. B. Wells, D. Plump & F. Kamareddine (2003):
Diagrams for Meaning Preservation.
In: RTA 2003,
LNCS 2706.
Springer,
pp. 88 –106,
doi:10.1007/3-540-44881-0_8.
A. K. Wright & M. Felleisen (1994):
A Syntactic Approach to Type Soundness.
Inf. Comput. 115(1),
pp. 38–94,
doi:10.1006/inco.1994.1093.
eptcs@eptcs.org