@article {Ariola:December 1997:0890-5401:154,
	author = "Ariola Z.M.",
	author = "Klop J.W.",
	title = "Lambda Calculus with Explicit Recursion",
	journal = "Information and Computation",
	volume = "139",
	year = "December 1997",
	abstract = "<P> This paper is concerned with the study of lambda-calculuswith explicit recursion, namely of cyclic lambda-graphs. Thestarting point is to treat a lambda-graph as a system of recursionequations involving lambda-terms and to manipulate such systemsin an unrestricted manner, using equational logic, just as ispossible for first-order term rewriting. Surprisingly, now theconfluence property breaks down in an essential way. Confluencecan be restored by introducing a restraining mechanism on thesubstitution operation. This leads to a family of lambda-graphcalculi, which can be seen as an extension of the family oflambdasigma-calculi (lambda-calculi with explicit substitution).While the lambdasigma-calculi treat the let-construct asa first-class citizen, our calculi support the letrec, a featurethat is essential to reason about time and space behavior offunctional languages and also about compilation and optimizationsof programs Copyright 1997 Academic Press</P>",
	pages = "154-233(80)",
	url = "http://www.ingentaconnect.com/content/ap/ic/1997/00000139/00000002/art02651"
}