14 citations · 25 across the 6 of their papers we have counts for
7 papers · 1 filter
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…
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…
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 …
On Computational Paths and the Fundamental Groupoid of a Type
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina de Oliveira
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computati…
On the Groupoid Model of Computational Paths
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences or rewrites', computati…
Sequences of Rewrites: A Categorical Interpretation
Arthur Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
In Martin-Löf's Intensional Type Theory, identity type is a heavily used and studied concept. The reason for that is the fact that it's responsible for the recently discovered conn…
Propositional equality, identity types, and direct computational paths
Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
In proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactic…