Prof. Ruy J. Guerra B. de Queiroz (Home Page)
Centro de Informática, Universidade Federal de Pernambuco, Brasil

Ruy de Queiroz received his B.Eng in Electrical Engineering from Escola Politecnica de Pernambuco (Recife, Brazil) in 1980, his M.Sc in Informatics from Universidade Federal de Pernambuco (UFPE) in 1984, and his Ph.D in Computing from the Imperial College, London in 1990. Currently a full professor at Centro de Informática of UFPE, with previous positions as Edward Larocque Tinker Visiting Professor, Philosophy, Stanford University, 2006; Research Associate, Department of Computing, Imperial College, London, 1989-1993, in his PhD thesis de Queiroz offered a reformulation of Martin-Lof's type theory based on a novel reading of Wittgenstein's "meaning-is-use" where the explanation of the consequences of a given proposition (formally, the reduction rules) gives the meaning to the logical constant dominating the proposition, amounting to a non-dialogical interpretation of logical constants via the effect of elimination rules over introduction rules, finding a parallel in Lorenzen's and Hintikka's dialogue/game-semantics. Since later in the 1990's de Queiroz has been engaged in a program of providing a general account of the functional interpretation of classical and non-classical logics via such an alternative theory of meaning for type theory, combined with D. Gabbay's notion of labeled deduction. As a result, alternative accounts of the functional interpretation of the existential quantifier, as well as the notion of propositional equality, were put forward, the latter allowing for a recasting of Statman's notion of direct computation, and a novel approach to the dichotomy "intensional versus extensional" accounts of propositional equality via the CurryHoward interpretation. A book entitled "The Functional Interpretation of Logical Deduction" (joint with A. de Oliveira and D. Gabbay) (World Scientific, 2011), gives a general perspective on such a research program. More recently, a categorical interpretation for such a formulation of propositional equality has been shown to be similar to the one given for homotopy type theory, namely that the identity type is the type of computational paths, and obeys the laws of groupoid.

Title: Propositional equality, identity types, and computational paths.
Abstract
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 syntactical details (such as, e.g., change of bound variables). When setting up a proof theory for equality one is faced with a rather unexpected situation where there may not be a unique canonical proof of an equality statement. Indeed, in a (1994-5) proposal for the formalisation of proofs of propositional equality in the Curry--Howard style, we have already uncovered such a peculiarity. Totally independently, and in a different setting, Hofmann & Streicher (1994) have shown how to build a model of Martin-Löf's Type Theory in which uniqueness of canonical proofs of identity types does not hold. The intention here is to show that, by considering as sequences of rewrites and substitution, it comes a rather natural fact that two (or more) distinct proofs may be yet canonical and are none to be preferred over one another. By looking at proofs of equality as rewriting (or computational) paths this approach will be in line with the recently proposed connections between type theory and homotopy theory via identity types, since elements of identity types will be, concretely, paths (or homotopies). Recent results giving a categorical interpretation of identity types as types of computational paths will also be touched upon, time permitting.