# Ruy de Queiroz

Ruy José Guerra Barretto de Queiroz (Recife, 11 de janeiro de 1958) é um professor titular da Universidade Federal de Pernambuco e possui trabalhos significativos nas áreas de pesquisa da Lógica matemática, Teoria da prova, Fundações da matemática e Filosofia da matemática. Ele é o fundador do WoLLIC (Workshop on Logic, Language, Information and Computation), que tem sido organizado anualmente desde 1994, tipicamente em Junho ou Julho.
Ruy de Queiroz recebeu seu Bacharelado em Engenharia Elétrica pela Escola Politecnica de Pernambuco in 1980, seu Mestrado em Ciências da Computação pela Universidade Federal de Pernambuco in 1984, e seu Doutorado em Computação pelo Imperial College em 1990, pela defesa da Dissertação "Proof Theory and Computer Programming. An Essay into the Logical Foundations of Computation"; supervisionado pelo Professor Thomas S. E. Maibaum.

## Perfil de pesquisa

No fim da década de 1980, Ruy de Queiroz ofereceu uma reformulação da teoria dos tipos de Martin-Lof baseada numa nova leitura do conceito 'significado é uso', de Wittgenstein, onde a explicação das consequências de uma dada proposição dá o significado da constante lógica dominante da proposição, equivalendo a uma interpretação não-dialógica de constantes lógicas por meio dos efeitos de regras da eliminação sobre regras de introdução, achando um paralelo com a lógica do diálogo de Lorenzen e Hintikka. Isso levou à uma teoria dos tipos chamada de 'Meaning as Use Type Theory’ (ou 'Teoria dos Tipos do Significado como Uso'). Em referência ao uso do dito de Wittgenstein, ele mostrou que o aspecto relativo à explicação das consequências de uma proposição data de muito tempo atrás, quando, em uma carta à Russell, Wittgenstein se refere ao quantificador universal como tendo significado apenas quando se vê o que está ligado a ele.
Desde a década de 1990, Ruy de Queiroz está engajado, juntamente com D. Gabbay, em um programa de fornecimento de uma consideração geral da interpretação funcional da lógica clássica e não-clássica por meio da noção de dedução natural. Como resultado, novas interpretações do quantificador universal, assim como a noção de igualdade proposicional, foram apresentadas, a última permitindo uma remodelação da noção de computação direta de Statman, e uma nova aproximação da dicotômica consideração 'intencional versus extensional' da igualdade proposicional por meio da interpretação de Curry-Howard.
Desde o começo dos anos 2000, Ruy de Queiroz vem investigando, juntamente com Anjolina de Oliveira, uma perspectiva geométrica da dedução natural apoiada numa consideração baseada em grafos da dedução natural simétrica de Kneale.

## Serviço à profissão

* Membro do Advisory Group to the Rolf Schock Prize in Logic and Philosophy (2008 e 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–presente;
* 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;
* Editor convidado de vários volumes (em parceria com vários lógicos e cientistas da computação como 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) de Annals of Pure and Applied Logic, Theoretical Computer Science, Information and Computation, Journal of Computer System and Sciences, Fundamenta Informaticae, Electronic Notes in Theoretical Computer Science;
* Criador e organizador da série de workshops WoLLIC (http://www.cin.ufpe.br/~wollic);
* Membro da Editorial Board of the International Directory of Logicians, D. Gabbay & J. Woods (eds.), College Publications;
* Membro eleito do Council da Association for Symbolic Logic, 2006-2008.

## Publicações chave

* (com de Oliveira, A.) The Functional Interpretation of Direct Computations. Electronic Notes in Theoretical Computer Science 269:19-40, 2011.
* On reduction rules, meaning-as-use, and proof-theoretic semantics, Studia Logica 90(2):211-247, Novembro de 2008.
* (com de Oliveira, A.) Geometry of Deduction via Graphs of Proof. Em Logic for Concurrency and Synchronisation, R. de Queiroz (ed.), volume 18 da série Trends in Logic, Kluwer Acad. Pub., Dordrecht, Julho de 2003, ISBN 1-4020-1270-5, pp. 3–88.
* Meaning, function, purpose, usefulness, consequences - interconnected concepts. Logic Journal of the Interest Group in Pure and Applied Logics, 9(5):693-734, Setembro de 2001, Oxford Univ. Press.
* (com Gabbay, D.) Labelled Natural Deduction. Em Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, H.J. Ohlbach and U. Reyle (eds.), volume 5 da série Trends in Logic, Kluwer Academic Publishers, Dordrecht, Junho de 1999, pp. 173–250.
* (com 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. Versão completa de um artigo apresentado na 2ª WoLLIC'95, Recife, Brasil, Julho de 1995. Abstract appeared in Journal of the Interest Group in Pure and Applied Logics 4(2):330-332, 1996.
* (com 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). Versão completa de um artigo apresentado no Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753-754, 1993.
* Normalisation and Language-Games. In Dialectica 48(2):83-123, 1994. (Versão prévia apresentada no Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
* (com Gabbay, D.) Extending the Curry-Howard interpretation to linear, relevant and other resource logics, in Journal of Symbolic Logic 57(4):1319-1365. Artigo apresentado no Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139-1140, 1991.
* Meaning as grammar plus consequences, in Dialectica 45(1):83-86.
* (com Maibaum, T.) Abstract Data Types and Type Theory: Theories as Types, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 37:149-166.
* (com Maibaum, T.) Proof Theory and Computer Programming, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 36:389-414.
* A Proof-Theoretic Account of Programming and the Rôle of Reduction Rules, in Dialectica 42(4):265-282.
* The mathematical language and its semantics: to show the consequences of a proposition is to give its meaning. In Weingartner, Paul and Schurz, Gerhard, editors, Reports of the Thirteenth International Wittgenstein Symposium 1988, volume 18 of Schriftenreihe der Wittgenstein-Gesellschaft, Vienna, 304pp. Hölder-Pichler-Tempsky, pp. 259–266. Symposium held in Kirchberg/Wechsel, Austria, August 14–21, 1988.
Na imprensa:
* de Queiroz, R. de Oliveira, A., & Gabbay, D.: 2011, The Functional Interpretation of Logical Deduction. Vol. 5 da série Advances in Logic. Imperial College Press / World Scientific. ISBN 978-981-4360-95-1. (2011).
* (with de Oliveira, A.) Propositional equality, identity types, and direct computational paths.

## Ensino

Ruy de Queiroz lecionou diversas disciplinas relacionadas a lógica e a ciência da computação teórica, incluindo Teoria dos Conjuntos, Teoria da Recursão (como uma continuação de um curso dado por), Lógica para Computação, Matemática Discreta, Teoria da Computação, Teoria da Prova, Fundações da Criptografia. Tem sete alunos doutores no ramo da Lógica Matemática e Ciência da Computação Teórica.

## Nomeações acadêmicas regulares

* Edward Larocque Tinker Visiting Professor, Department of Philosophy, Stanford University 2005-6.
* Professor Associado, Universidade Federal de Pernambuco, Recife, Brazil, 1993–present.

## Honras e prêmios

* Edward Larocque Tinker Visiting Professorship na Stanford University, premiado por The Tinker Foundation, após ser nomeado por Solomon Feferman e Grigori Mints, 2005;
* Overseas Research Student, Committee of Vice-Chancellors and Principals, University of London, 1985-1987.