A formalised first-order confluence proof for the λ-calculus using one-sorted variable names
René Vestergaard, James BrotherstonVolume:
183
Year:
2003
Language:
english
Pages:
33
DOI:
10.1016/s0890-5401(03)00023-3
File:
PDF, 464 KB
english, 2003