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]
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.
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]
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.