Ruy de Queiroz

Ruy J. Guerra B. de Queiroz (born January 11, 1958, in Recife) 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.^[1] He is the founder of the Workshop on Logic, Language, Information and Computation (WoLLIC), 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.

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".^[2] 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.^[3]

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.^[4]

• Member of the Advisory Group to the Rolf Schock Prize in Logic and Philosophy (2008 and 2011) Prize Committee (Royal Swedish Academy of Sciences);
• Editor-in-chief, Logic Journal of the Interest Group in Pure and Applied Logics, Oxford University Press, 1993–present;
• Associate editor, Journal of Computer System and Sciences, coordinator and co-founder (with D. Gabbay), Interest Group in Pure and Applied Logics (IGPL), the clearing house of the European Association for Logic, Language and Information (FoLLI), 1990–present;
• Guest editor of several volumes (in partnership with several world standing logicians and computer scientists such as John Baldwin, Sergei N. Artemov, Bruno Poizat, Dexter Kozen, Angus Macintyre, Grigori Mints, Wilfrid Hodges, Anuj Dawar, Hiroakira Ono, Makoto Kanzawa, Daniel Leivant, Lev Beklemishev) of Annals of Pure and Applied Logic, Theoretical Computer Science, Information and Computation, Journal of Computer System and Sciences, Fundamenta Informaticae, several volumes of Electronic Notes in Theoretical Computer Science;
• Creator and prime organizer of the series of workshops WoLLIC (http://www.cin.ufpe.br/~wollic);
• Member of the editorial board of the International Directory of Logicians, D. Gabbay & J. Woods (eds.), College Publications;
• Elected member, Council, Association for Symbolic Logic, 2006-2008.

1. (with de Oliveira, A.) 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(2):211-247, November 2008.
3. (with de Oliveira, A.) Geometry of Deduction via Graphs of Proof. In Logic for Concurrency and Synchronisation, R. de Queiroz (ed.), volume 18 of the Trends in Logic series, Kluwer Acad. Pub., Dordrecht, July 2003, ISBN 1-4020-1270-5, pp. 3–88.
4. Meaning, function, purpose, usefulness, consequences - interconnected concepts. Logic Journal of the Interest Group in Pure and Applied Logics, 9(5):693-734, September 2001, Oxford Univ. Press.
5. (with Gabbay, D.) Labelled Natural Deduction. In Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, H.J. Ohlbach and U. Reyle (eds.), volume 5 of Trends in Logic series, Kluwer Academic Publishers, Dordrecht, June 1999, pp. 173–250.
6. (with de Oliveira, A.) A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction. Logic Journal of the Interest Group in Pure and Applied Logics, 7(2):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(2):330-332, 1996.
7. (with Gabbay, D.) The Functional Interpretation of the Existential Quantifier, in Bulletin of the Interest Group in Pure and Applied Logics 3(2-3):243-290, 1995. (Special Issue on Deduction and Language, Guest Editor: Ruth Kempson). Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753-754, 1993.
8. Normalisation and Language-Games. In Dialectica 48(2):83-123, 1994. (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
9. (with Gabbay, D.) Extending the Curry-Howard interpretation to linear, relevant and other resource logics, in Journal of Symbolic Logic 57(4):1319-1365. Paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139-1140, 1991.
10. (with Maibaum, T.) Abstract Data Types and Type Theory: Theories as Types, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 37:149-166.
11. (with Maibaum, T.) 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(4):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. ISBN 978-981-4360-95-1.

Ruy de Queiroz has taught several disciplines related to logic and theoretical computer science, including Set Theory, Recursion Theory (as a follow-up to a course given by Solomon Feferman), 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.

• Tinker Visiting Professorship at Stanford University, awarded by The Tinker Foundation, after the nomination given by Solomon Feferman and Grigori Mints, 2005;
• Overseas Research Student scholarship award, Committee of Vice-Chancellors and Principals, University of London, 1985-1987.

• Ruy Guerra's professional profile home page