Under consideration for publication in J. Functional Programming 1 (2008)
Big-step Normalisation, Thorsten Altenkirch, James Chapman
Traditionally, decidability of conversion for typed λ-calculi is established by showing that small-step reduction is confluent and strongly normalising. Here we investigate an alternative approach...