Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus. - Matthias Mann 001 (SOS@CONCUR, 2004)

A non-deterministic call-by-need lambda calculus: proving similarity a precongruence by an extension of Howe's method to sharing. - Matthias Mann 001 (2005)

Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi. - Matthias Mann 001; Manfred Schmidt-Schauß (Inf. Comput., 2010)