A formalised first-order confluence proof for the -calculus using one-sorted variable names

René Vestergaard, James Brotherston. A formalised first-order confluence proof for the -calculus using one-sorted variable names. Inf. Comput., 183(2):212-244, 2003. [doi]

Abstract

Abstract is missing.