14 citations · 30 across the 16 of their papers we have counts for
12 papers · 1 filter
A Theory of a Two-Dimensional Typed Lambda Calculus
Daniel O. Martínez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
We present a typed two-dimensional -calculus whose equality evidence is \emph{computational}: a path between two terms is an explicit finite sequence of one-step conversions (th…
Topological Computational Paths: Presentation Invariance and Observable Quotients
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira +1
A computational path records the steps used to establish an equality. Topologies on computational equality witnesses can depend on the chosen generators and execution schedule, eve…
The Theory of an Arbitrary Higher -Model
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
One takes advantage of some basic properties of every homotopic -model (e.g.\ extensional Kan complex) to explore the higher -conversions, which would correspond to proofs o…
Solving Homotopy Domain Equations
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
In order to get -models with a rich structure of -groupoid, which we call "homotopy -models", a general technique is described for solving domain equations on any car…
Towards a Homotopy Domain Theory
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
An appropriate framework is put forward for the construction of -models with -groupoid structure, which we call \textit{homotopic -models}, through the use of an $\in…
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…