Valeria de Paiva | |
---|---|
Born | Valeria Correa Vaz de Paiva |
Alma mater | University of Cambridge (PhD) |
Scientific career | |
Fields | |
Institutions | PARC Nuance Communications University of Birmingham |
Thesis | The Dialectica Categories (1988) |
Doctoral advisor | Martin Hyland [2] |
Website | vcvpaiva |
Valeria Correa Vaz de Paiva is a Brazilian mathematician, logician, and computer scientist. Her work includes research on logical approaches to computation, especially using category theory, knowledge representation and natural language semantics, and functional programming with a focus on foundations and type theories. [3] [4] [5]
De Paiva earned a bachelor's degree in mathematics in 1982, [3] a master's degree in 1984 (on pure algebra) and completed a doctorate at the University of Cambridge in 1988, under the supervision of Martin Hyland. [6] [2] Her thesis introduced Dialectica spaces, a categorical way of constructing models of linear logic, based on Kurt Gödel's Dialectica interpretation.
She worked for nine years at PARC in Palo Alto, California, and also worked at Rearden Commerce and Cuil before joining Nuance. [4] [7] She is an honorary research fellow in computer science at the University of Birmingham. [1] [7] She is currently on the Council of the Division for Logic, Methodology and Philosophy of Science and Technology of the International Union of History and Philosophy of Science and Technology (2020–2023). [8]
Stephen Cole Kleene was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of mathematical logic known as recursion theory, which subsequently helped to provide the foundations of theoretical computer science. Kleene's work grounds the study of computable functions. A number of mathematical concepts are named after him: Kleene hierarchy, Kleene algebra, the Kleene star, Kleene's recursion theorem and the Kleene fixed-point theorem. He also invented regular expressions in 1951 to describe McCulloch-Pitts neural networks, and made significant contributions to the foundations of mathematical intuitionism.
Dana Stewart Scott is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California. His work on automata theory earned him the Turing Award in 1976, while his collaborative work with Christopher Strachey in the 1970s laid the foundations of modern approaches to the semantics of programming languages. He has also worked on modal logic, topology, and category theory.
Linear logic is a substructural logic proposed by French logician Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.
Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes.
Samson Abramsky is a British computer scientist who is a Professor of Computer Science at University College London. He was previously the Christopher Strachey Professor of Computing at Wolfson College, Oxford, from 2000 to 2021.
Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970.
Kit Fine is a British philosopher, currently university professor and Silver Professor of Philosophy and Mathematics at New York University. Prior to joining the philosophy department of NYU in 1997, he taught at the University of Edinburgh, University of California, Irvine, University of Michigan and UCLA. The author of several books and dozens of articles in international academic journals, he has made notable contributions to the fields of philosophical logic, metaphysics, and the philosophy of language and also has written on ancient philosophy, in particular on Aristotle's account of logic and modality.
Chu spaces generalize the notion of topological space by dropping the requirements that the set of open sets be closed under union and finite intersection, that the open sets be extensional, and that the membership predicate be two-valued. The definition of continuous function remains unchanged other than having to be worded carefully to continue to make sense after these generalizations.
Burton Spencer Dreben was an American philosopher specializing in mathematical logic. A Harvard graduate who taught at his alma mater for most of his career, he published little but was a teacher and a critic of the work of his colleagues.
Michael Paul Fourman is Professor of Computer Systems at the University of Edinburgh in Scotland, UK, and was Head of the School of Informatics from 2001 to 2009.
(John) Martin Elliott Hyland is professor of mathematical logic at the University of Cambridge and a fellow of King's College, Cambridge. His interests include mathematical logic, category theory, and theoretical computer science.
Ursula Hilda Mary Martin is a British computer scientist, with research interests in theoretical computer science and formal methods. She is also known for her activities aimed at encouraging women in the fields of computing and mathematics. Since 2019, she has served as a professor at the School of Informatics, University of Edinburgh.
Dialectica spaces are a categorical way of constructing models of linear logic.
In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic logic into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic. The name of the interpretation comes from the journal Dialectica, where Gödel's paper was published in a 1958 special issue dedicated to Paul Bernays on his 70th birthday.
Peter Henry George Aczel was a British mathematician, logician and Emeritus joint Professor in the Department of Computer Science and the School of Mathematics at the University of Manchester. He is known for his work in non-well-founded set theory, constructive set theory, and Frege structures.
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 (WoLLIC), which has been organised annually since 1994, typically in June or July.
Eugenia Loh-Gene Cheng is a British mathematician, educator and concert pianist. Her mathematical interests include higher category theory, and as a pianist she specialises in lieder and art song. She is also known for explaining mathematics to non-mathematicians to combat math phobia, often using analogies with food and baking. Cheng is a scientist-in-residence at the School of the Art Institute of Chicago.
Applied category theory is an academic discipline in which methods from category theory are used to study other fields including but not limited to computer science, physics, natural language processing, control theory, probability theory and causality. The application of category theory in these domains can take different forms. In some cases the formalization of the domain into the language of category theory is the goal, the idea here being that this would elucidate the important structure and properties of the domain. In other cases the formalization is used to leverage the power of abstraction in order to prove new results about the field.
Thomas Edward Forster is a British set theorist and philosopher. His work has focused on Quine's New Foundations, the theory of well-quasi-orders and better-quasi-orders, and various topics in philosophy.