Computational Paths -- An approach in the $LN{D}_{EQ}-TR{S}_2$ system

Tiago M. L. Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1

We use a labelled deduction system ( LND${}_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which al…