Ruy de Queiroz


Ruy J. Guerra B. de Queiroz is an associate professor at Universidade Federal de Pernambuco and holds significant works in the research fields of Mathematical logic, proof theory, foundations of mathematics and philosophy of mathematics. He is the founder of the Workshop on Logic, Language, Information and Computation, which has been organised annually since 1994, typically in June or July.
Ruy de Queiroz received his B.Eng in Electrical Engineering from Escola Politecnica de Pernambuco in 1980, his M.Sc in Informatics from Universidade Federal de Pernambuco in 1984, and his Ph.D in Computing from the Imperial College, London in 1990, for which he defended the Dissertation Proof Theory and Computer Programming. An Essay into the Logical Foundations of Computation.

Research profile

In the late 1980s, Ruy de Queiroz has offered a reformulation of Martin-Löf type theory based on a novel reading of Wittgenstein’s "meaning-is-use", where the explanation of the consequences of a given proposition gives the meaning to the logical constant dominating the proposition. This amounts to a non-dialogical interpretation of logical constants via the effect of elimination rules over introduction rules, which finds a parallel in Paul Lorenzen's and Jaakko Hintikka's dialogue/game-semantics. This led to a type theory called "Meaning as Use Type Theory". In reference to the use of Wittgenstein's dictum, he has shown that the aspect concerning the explanation of the consequences of a proposition is present since a very early date when in a letter to Bertrand Russell, where Wittgenstein refers to the universal quantifier only having meaning when one sees what follows from it.
Since later in the 1990s, Ruy de Queiroz has been engaged, jointly with Dov Gabbay, in a program of providing a general account of the functional interpretation of classical and non-classical logics via the notion of labeled natural deduction. As a result, novel 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 Richard Statman's notion of direct computation, and a novel approach to the dichotomy "intensional versus extensional" accounts of propositional equality via the Curry–Howard correspondence.
Since the early 2000s, Ruy de Queiroz has been investigating, jointly with Anjolina de Oliveira, a geometric perspective of natural deduction based on a graph-based account of Kneale's symmetric natural deduction.

Service to the profession

  1. The Functional Interpretation of Direct Computations. Electronic Notes in Theoretical Computer Science 269:19-40, 2011.
  2. On reduction rules, meaning-as-use, and proof-theoretic semantics, Studia Logica 90:211-247, November 2008.
  3. Geometry of Deduction via Graphs of Proof. In Logic for Concurrency and Synchronisation, R. de Queiroz, volume 18 of the Trends in Logic series, Kluwer Acad. Pub., Dordrecht, July 2003,, pp. 3–88.
  4. Meaning, function, purpose, usefulness, consequences - interconnected concepts. Logic Journal of the Interest Group in Pure and Applied Logics, 9:693-734, September 2001, Oxford Univ. Press.
  5. Labelled Natural Deduction. In Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, H.J. Ohlbach and U. Reyle, volume 5 of Trends in Logic series, Kluwer Academic Publishers, Dordrecht, June 1999, pp. 173–250.
  6. A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction. Logic Journal of the Interest Group in Pure and Applied Logics, 7:173-215, 1999, Oxford Univ. Press. Full version of a paper presented at 2nd WoLLIC'95, Recife, Brazil, July 1995. Abstract appeared in Journal of the Interest Group in Pure and Applied Logics 4:330-332, 1996.
  7. The Functional Interpretation of the Existential Quantifier, in Bulletin of the Interest Group in Pure and Applied Logics 3:243-290, 1995.. Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58:753-754, 1993.
  8. Normalisation and Language-Games. In Dialectica 48:83-123, 1994.
  9. Extending the Curry-Howard interpretation to linear, relevant and other resource logics, in Journal of Symbolic Logic 57:1319-1365. Paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56:1139-1140, 1991.
  10. Abstract Data Types and Type Theory: Theories as Types, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 37:149-166.
  11. Proof Theory and Computer Programming, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 36:389-414.
  12. A Proof-Theoretic Account of Programming and the Rôle of Reduction Rules, in Dialectica 42:265-282.
  13. de Queiroz, R. de Oliveira, A., & Gabbay, D.: 2011, The Functional Interpretation of Logical Deduction. Vol. 5 of Advances in Logic series. Imperial College Press / World Scientific..

    Teaching

Ruy de Queiroz has taught several disciplines related to logic and theoretical computer science, including Set Theory, Recursion Theory, Logic for Computer Science, Discrete Mathematics, Theory of Computation, Proof Theory, Model Theory, Foundations of Cryptography. He has had seven Ph.D. students in the fields of Mathematical Logic and Theoretical Computer Science.

Honors and awards