Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Valeria de Paiva

Valeria de Paiva

Valeria de Paiva is a research scientist at the Systems and Practices Laboratory (SPL)
of PARC (Palo Alto Research Center), California.PARC.
She received her PhD in Mathematics from Cambridge University in 1988 for work on "Dialectica Categories" ,
under Martin Hyland's supervision, and has ever since worked on logical approaches to computation, especially using Category Theory.

Honorary Research Fellow at the School of Computer Science, University of Birmingham, UK.

Email: paiva at parc.com.

Research Interests

Categorical Proof theory
Linear Logic and Intuitionistic Modal logics
Logics for Knowledge Representation (KXDC)
Logics of Context
Typed Lambda Calculi
Semantics of Programming Languages
Formal Aspects of Computer Security
Linguistic Applications of Linear Logic
Automated Deduction
Categories in Concurrency Theory

[ Publications ] [ Curriculum Vitae ] [ Past Meetings ] [ Teaching ]

Meetings

CONTEXT'05 July 5-8, 2005, Paris, France. Member of Programme Committee.
Context Representation and Reasoning (CRR'05), Paris, 5th July 05. Member of Programme Committee.
IMLA'05: Workshop associated with LICS'05, June, 30th, 2005, Chicago, Illinois, USA. Organizer with F. Pfenning.
First World Conference and School on Universal Logic 26th March - 3rd April, 2005, Montreux, Switzerland. Invited Speaker.
ESSLLI 2004 - The 16th European Summer School in Logic, Language and Information Course organiser.
The reader for this course contains the material to be covered. Here I'm listing some more advanced material.
Lecture notes for previous course on categorical models of Linear Logic, algebraic semantics (lineales), relating categorical semantics.
Also Phil Scott survey article on models of LL, Bierman's clear account of a model, Alexiev's survey of LL applications (somewhat outdated in 2004).
Category Theory in Computer Science (CTCS 2004) Member of Programme Committee.
CONTEXT'03 Chairperson of a session on Logics of Context.
Also of Barwise and Situation Semantics, a co-located workshop organized by Tim Fernando.
Intuitionistic Modal Logics and Applications (IMLA'02) (Organizer) Workshop at FLoC'02.
Here you can find the beginnings of a bibliography on constructive modal logics and applications.
Natural Deduction 2001, PUC Rio, June 2001, Invited Speaker, organised by L. C. Pereira.

Editorial Work

Editorial Board of LOMECS, Logical Methods in Computer Science .
Editorial Board of TAC, Theory and Applications of Categories .
Guest Editor for a volume of the Journal of Logic and Computation on Intuitionistic Modal Logics and Applications, with Michael Mendler and Rajeev Gore.
Guest Editor for a special volume of Theory and Applications of Categories on Chu Spaces: Theory and Applications with Vaughan Pratt.
Advances in Natural Deduction (provisional title) Editor of a special volume organised with L. C. Pereira and H. E. Hausler.

Research Projects

RDC Reasoning about Document Collections

Hybrid Logic Meets Other Logics (HyLoMOL)

Intuitionistic Modal Logics and Applications. Informal research project with several collaborators, including Torben Brauner, Gianluigi Bellin, Eike Ritter, Michael Mendler, Rajeev Gore, Natasha Alechina, Frank Pfenning, Neil Ghani and Milly Maietti.
xSLAM: an abstract machine for Linear Functional Programming
Together with Eike Ritter, Neil Ghani (now at Leicester), Milly Maietti, Francisco Alberti (now at ENS, Paris) and Paola Maneggia I helped develop xLIN, a linear abstract machine, based on a calculus of explicit substitutions. You can read about this EPSRC project in the xSLAM page. This project finished in March 2000, you can read a short summary here.
Formal Verification using Subtructural Logics
Together with Saraswati Kalvala and Eike Ritter and Milly Maietti I am thinking about substructural logics for formal verification. This builds on our previous collaboration on mechanising Linear Logic in Isabelle, but the project is "on the back burner" for the time being.
Full Intuitionistic Linear Logic
Together with Torben Brauner, Eike Ritter and Milly Maietti, I started working on building up the foundations of Full Intuitionistic Linear Logic. This project has been in the "back burner" for a while.
The theory group in Birmingham has academic links with the EU-funded TYPES and APPSEM working groups.
We also had a British Council small collaborative project with the teams at Nancy and ENS (Paris), France.
We strongly support the British Logic Colloquium, and hope it will become more widely known as time goes by.

Collaborators

I do like to work with other people. Here is an incomplete (and vaguely chronological) list of people I am working with/have worked with:

Personal

I am a Brazilian, who misses very much Rio de Janeiro. My old `alma mater' is PUC in Rio.
But my work `alma mater' is Cambridge, where I spent 11 years.
I am especially fond of the computer laboratory.

I have a lovely daughter, a beautiful son and a great husband.
A few pictures of the kids are here.