3 papers
cs.LO2020
Computational Paths -- An approach in the system
Tiago M. L. Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
We use a labelled deduction system ( LNDTRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which al…
cs.LO2019
A Topological Application of Labelled Natural Deduction
Tiago M. L. Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewri…
cs.LO2016
Explicit Computational Paths
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms of a type …