Valeria de Paiva
BS Mathematics, 1978
MSc Algebra, 1984
Part III, 1985
PhD Mathematics, 1988
Cambridge University, UK
Natural Language Theory and Technology Group (NLTT)
I am a research scientist at the Natural Language Theory and Technology (NLTT) group of the Intelligent Systems Laboratory of the fabled PARC (Palo Alto Research Center), which used to be called Xerox PARC. PARC is famous for such innovations as laser printing, distributed computing and Ethernet, the graphical user interface (GUI), object-oriented programming, and ubiquitous computing, for example. But of course, I cannot take any credit for that, it all happened long before I arrived. In PARC we're fond of saying that “we invent the future”, which is not a bad motto, if you ask me.
I am a Brazilian, from Rio de Janeiro, but I got my doctorate in Mathematics in Cambridge, UK, for work on "Dialectica Categories" written under Martin Hyland's supervision. Working in Cambridge was a life-changing experience: I am now proud to say that my "academic great-grandfather" is none less than the founder of theoretical computer science, Alan Turing. I have, since my Cambridge days, worked on logical approaches to computation. My research interests include categorical proof theory, type theory, programming languages, logics for knowledge representation, logics of context, linear logic, intuitionistic modal logics and linguistic applications of logic. My work spans several different fields and I like all of my 'hats': mathematician, logician, computer scientist and more recently computational linguist.
I'm on the editorial boards of the journals "Theory and Applications of Categories", "Logical Methods in Computer Science" and "Logica Universalis", as well as on the editorial boards of the Springer-Verlag new series "Logic, Language and Information" and of Polimetrica's "Category Theory".
My recent work focuses on uncovering the logical structure of representations of unstructured texts, and on building appropriate logics for these representations, using contexts. The goal is to build logics that reflect the way language is used, are sound, tractable, and whose proofs provide traces that make it understandable by people. One of my linguist friends says that the problem of asking logicians for logics of language is that they're like tailors that when asked for a pair of trousers (my friend lives in Edinburgh, Scotland) always reply but I make wonderful shirts, wouldn't you like to try this one? And indeed the shirts are wonderful, but not quite what you need. Thus this business of logics for language, with the properties desired, is a tall order, but I'm having fun trying to get there.