Publications of Valeria de Paiva
- Categorical Semantics of Linear Logic for
All, Manuscript, (submitted 2006).
- Bridges from Language to Logic: Concepts, Contexts and
Ontologies (V. de Paiva) in 5th Logical and Semantic
Frameworks with Applications, LSFA'10, parte of ICTAC in Natal,
- Constructive Description Logic, Hybrid-Style (V. de Paiva,
H. Hausler e A. Rademaker), in Pre-proceedings of the International Workshop on
Hybrid Logic and Applications (HyLo 2010), Aug 2010.
- Using Intuitionistic Logic as a basis for Legal Ontologies (H.
Hausler, A. Rademaker e V. de Paiva), in ``Proceedings of Legal Ontologies and
Artificial Intelligence Techniques (LOAIT)", July 2010.
- Logic, Language, Information and Computation, special issue of
the journal Information and Computations, guest editors: G. Mints,
Valeria de Paiva and R. de Queiroz, online 3 September 2009. DOI
- Context Inducing Nouns, (with
Charlotte Price and Tracy H. King), in Knowledge and
Reasoning for Answering Questions (KRAQ'08) workshop associated
with COLING'08, Manchester, UK, 23 August 2008, preliminary version.
- Designing Testsuites for Grammar-based
Systems in Applications (with Tracy H. King), in Workshop
on Grammar Engineering Across Frameworks (GEAF'08), Manchester,
UK, 24 August 2008, first version.
- Existential implications of transitive verbs: a preliminary
classification for textual inference (with Patricia Amaral, Cleo
Condoravdi and Annie Zaenen), manuscript, June 2008.
- Consequence-informed access control, (with Jessica Staddon),
short note for Xerox Innovation Group (XIG) Research and Technology
Conference, May 2008.
- Deverbal Nouns in Knowledge Representation.
Comput. 18(3): 385-404 (2008).
Institutional View of Categorical Logic and the Curry-Howard-Tait
Isomorphism (with Joseph Goguen, Till Mossakowski, Florian Rabe,
and Lutz Schröder). In Int J Software Informatics, 1 (1), pp.
and Question Answering System
(with Daniel G. Bobrow, Bob Cheslow, Cleo Condoravdi, Lauri Karttunen,
Tracy H. King, Rowan Nairn, Charlotte Price and Annie Zaenen).
Proceedings of Grammar Engineering Across Frameworks, pp 26--45, 2007.
2007 Proceedings of the Workshop (editor with Patrick Blackburn,
Joergen Villadsen). Electr.
Theor. Comput. Sci. 174(6): 1-2 (2007).
Logic: Take Two, (with D. G. Bobrow, C. Condoravdi, R.
Karttunen, T. H. King, R. Nairn and A. Zaenen) Proceedings of the Workshop on Contexts
and Ontologies, Representation and Reasoning, CONTEXT 2007.
Inference (with Bobrow, D. G.,
C. Condoravdi, L. Karttunen, T. H. King, L. Price, R.
L.Price, A. Zaenen) Proceedings
ACL-PASCAL Workshop on Textual
Entailment and Paraphrasing, pp. 16-21, 2007.
Description Logics: what, why and
how. (extended draft) Presented at Context Representation and
Reasoning, Riva del Garda, August 2006.
- Constructive hybrid logics and contexts. Hybrid Logics Workshop
(HYLO 2006); Invited Talk, August 11, 2006; Seattle, WA; USA.
- Deverbal Nouns in Knowledge Representation
(with O. Gurevich, D. Crouch, and T. H. King), Appeared in
FLAIRS (The Florida Artificial Intelligence Research Society),
May 11-13, 20006 and won one of the Best Paper Awards in FLAIRS
(apparently there were two...).
- A short note on Intuitionistic Propositional
Logic with Multiple Conclusions (with Luiz Carlos Pereira)
Manuscrito-- Rev Int. Fil. Campinas, v. 28, n.2, pp 317-329,
jul-dez, 2005. Word version.
of the special volume on Chu Spaces:
theory and applications (with Vaughan Pratt), Theory and
Applications of Categories, Vol. 17, 2006, No.7, pp 1-9.
Cousins?Theory and Applications of Categories, Vol. 17,
2006, No. 7, pp 127-152.
Parigot-style Linear Lambda-calculus
Intuitionistic Linear Logic (with Eike Ritter),Theory and
Applications of Categories, Vol. 17, 2006, No.3, pp 30-48.
(with T. Brauner), Presented at
Methods for Modalities 3, LORIA, Nancy, France, September 22-23,
2003. Also appears as a
report from the University of
- Full paper from above, submitted with new title Intuitionistic
Journal of Applied Logic(JAL). Appeared as JAL 4(2006), 231-- 255,
available online from the publishers on 11th August 2005.
Apparently it got to be the 2nd hottest
paper from that journal, but it has now disappeared from the hot spot..
Contexts (with Michael Mendler), In
Proceedings of the Worskhop on Context Representation and Reasoning,
Paris, France, July
Logic for Textual inference
(with D. Bobrow, C. Condoravdi, R. Crouch, R. Kaplan,
L. Karttunen, T. King and A. Zaenen),
In Procs. of the AAAI Workshop on Inference for Textual Question
Answering, Pittsburgh PA, July 2005.
(with Michael Mendler),
Abstract in the ASL Meeting in Stanford, March 2005.
Logics: the categorical
proof theory perspective
Abstract of an Invited Talk at Universal Logic, March 2005.
Intuitionistic Predicate Logic (with Milly Maietti)
Abstract of talk presented at Universal Logic 2005.
Intuitionistic Linear Logic
(with P. Maneggia and M. Maietti and E. Ritter), Invited Talk at
Natural Deduction 2001, Rio de Janeiro. Journal paper in Applied
Categorical Structures, volume 13(1):1--36, 2005.
- Towards constructive description logics. Talk at the Workshop on
Modal Logics and Applications (IMLA2005), associated with LiCS 2005.
- Intuitionistic Modal Logic and Application
(Special Issue) Journal of Logic and Computation, volume 14, number
4, August 2004. Guest Editors: Valeria de Paiva, Rajeev Gore' and
Michael Mendler. The (long) preface is below.
and Type Theories Preface to the special issue on
Intuitionistic Modal Logic and
Application of the Journal of Logic and Computation, volume 14, number
4, August 2004. Guest Editors: Valeria de Paiva, Rajeev Gore' and
- Logics of Context and Modal Type Theories. Mathematical
Foundantions of Programming Semantics (Talk); 2004 May; Pittsburgh; PA;
or, How to build models for
(with Andrea Schalk), Theoretical Computer Science 315 (2004) 83-107,
and Context as
(Constructive) Modality. In Modeling and Using Context,
Proceedings of the 4th International
and Interdisciplinary Conference CONTEXT 2003, Stanford, CA, USA,
Springer Lecture Notes in Artificial Intelligence, vol 2680, June
Understanding (with Cleo Condoravdi, Richard Crouch, Reinhard
Stolle, Daniel G. Bobrow.) Proceedings Human Language Technology
Conference (HLT-NAACL-2003), Workshop on Text Meaning, Edmonton,
Canada, May 2003.
Questions. (with Reinhard Stolle, Daniel Bobrow, Cleo
Condoravdi, Richard Crouch) Proceedings AAAI Spring Symposium on New
Directions in Question Answering, Stanford, California, March 2003.
(with Daniel Bobrow, Cleo Condoravdi, Richard Crouch and Reinhard
Stolle.) Abstract accompanying a talk at the Stanford Semantics and
Pragmatics Workshop, Stanford, California, March 2003.
- Intuitionistic Modal Logic and Applications (IMLA'02)
Workshop Proceedings. (eds. R. Gore, M. Mendler and V. de Paiva).
from the University of Bamberg, Germany, July 2002.
in Rudimentary Linear
(with M. Maietti and E. Ritter), presented at the Workshop on Implicit
Computational Complexity, FLoC'02, Copenhagen, 2002. Also technical
report of the University of Padova, Italy, 2002.
and categories in the
semantics of Linear Logic. Presented at LLC8, Stanford, May 1999.
Revised version (June 2000) appears in CSLI book "Words, Proofs, and
Diagrams" (eds. D. Barker-Plummer, D. Beaver, Johan van Benthem and P.
Scotto di Luzio), 2002.
Original version Lineales:
Linear Logic from a Categorical Perspective.
redundancy detection in
focused document collections.
(with Richard Crouch, Cleo Conodoravdi, Reinhard Stolle, Tracy King,
John Everett & Daniel Bobrow) Proceedings of Workshop on
Scalability in Natural Language Understanding (ScaNaLU), Heidelberg,
- Making Ontologies Work for Resolving Redundancies Across
(with J. Everett and D. Bobrow and C. Condoravdi and D. Crouch and M.
van der Berg and L. Polanyi), in "Communications of the ACM", February
2002, vol 45, number 2.
- Finding Similar Content within Different Documents (with J. O.
Everett, D. G. Bobrow, C. Condoravdi, R. Crouch and R. Stolle), in Mining
Answers from Texts and Knowledge Bases, Papers from 2002 AAAI
Spring Symposium, Eds. Sanda M. Harabagiu and Vinay Chaudhri, 2002.
Correspondence for a
Basic Constructive Modal Logic
(with G. Bellin and E. Ritter), In Methods for Modalities 2001,
Amsterdam, November 2001. (pdf)
(with C. Condoravdi, D. Crouch, J. Everett, R. Stolle, D. Bobrow,
M. van den Berg), In Proceedings of Formal Ontology in Information
Systems, FOIS'01, October 2001 (this is a preliminary version of the
Kripke Semantics for
Constructive S4 Modal Logic
(with Natasha Alechina and and Michael Mendler and Eike Ritter). In
Proc. of Computer Science Logic (CSL'01), LNCS 2142, ed L. Fribourg.
2001. (This is a corrected version of "Relating Categorical and Kripke
Semantics for Intuitionistic Modal Logics" below.)
- Soundness and completeness are not enough (linear type theories
their models) Invited talk. Logic, Language and Computation (10th LLC);
2001 May 26;
- Abstract algebraic substructural logics (talk). Stanford
University/Computer Science Dept. Theory Lunch; 2001 May 24; Stanford,
- On an
Intuitionistic Modal Logic
(with Gavin Bierman), Studia Logica (65):383-416, 2000.
(with Neil Ghani and Eike Ritter), in the Journal of the IGPL, vol 8,
Issue 1, January 2000, 7-31.
for Linear and
Intuitionistic Type Theory
(with Milly Maietti and Eike Ritter), In Proceedings of FOSSACS2000:
Foundations of Software Science and Computation Structures, Lecture
Notes in Computer Science, Springer-Verlag, vol 1784, April 2000.
for Linear Logical Frameworks
(with Iliano Cervesato and Eike Ritter), Proc. Workshop on Logical
Frameworks and Meta-Languages, September 1999.
(with Eike Ritter), Proc. WESTAPP-99, 1999.
of Linear Logic
(with Andrea Schalk), Proc. AMAST-99, LNCS 1548, 1999.
- Constructive Authentication Logics: a research proposal
In PRATICA: Proofs, Types and Categories, eds. E. H. Hausler and L. C.
of Explicit Substitutions
(with Neil Ghani and Eike Ritter), Proc FOSSACS-99, LNCS 1578,
and Kripke Semantics for Intuitionistic Modal
Logics (with Natasha Alechina and Eike Ritter). Proc. AiML II
(Advances in Modal Logic), 1998. NOTE: this paper had a serious bug,
which was corrected with the help of M. Mendler and M. Fairtlough.
Hence it's not down-loadable any more, but see the corrected version above.
Necessity (with Neil
Ghani and Eike Ritter), presented at 25th International Colloquium on
Automata, Languages and Programming (ICALP'98). Lecture Notes in
Computer Science LNCS 1443, eds. Larsen, Skyum and Winskel, 1998. This
is also available as a technical report.
(with Neil Ghani and Eike Ritter). Presented at Westapp'98. Also
Invited Talk at WOLLIC'98. A full version is available as
Technical Report CSR-98-02 . Superseded by the paper in the
Journal of the IGPL above.
from a Logical Perspective I. (with Benton and Bierman)
Journal of Functional Programming, 8(2):177-193. March 1998 .
- A Formulation of Linear Logic Based on
Dependency-Relations (with Torben Brauner) Proceedings of
Annual Conference of the European Association for Computer Science
Logic, Aarhus, Denmark, LNCS 1414, Springer-Verlag, 1997.
Explicit Substitutions and Names
(with Eike Ritter).
Presented at ICALP'97, LNCS 1256 eds. Degano, Gorrieri and
Marchetti-Spaccamela. Also Technical Report CSR-97-5, School of
Computer Science, University of Birmingham. March 1997.
(with Gavin Bierman).
Technical Report CSRP-96-10, School of Computer Science, University of
Birmingham. June 1996.
(Updated version of paper in Applied Logic Conference, Amsterdam, 1992.
Improved version appears as Studia Logica paper, 2000.)
Intuitionistic Linear Logic. (with Brauner). Technical Report
395 from Computer Laboratory, University of Cambridge and BRICS,
Denmark. May 1996.
Model of State.
(with Correa and Haeusler). In CATS'96, Computing: The Australian
Theory Symposium Proceedings, Melbourne, Australia, January 1996.
Logic in Isabelle (with S. Kalvala) in Proceedings of the
Isabelle Users Workshop, Technical Report TR379, Computer Laboratory,
University of Cambridge, September 1995.
- Yet another intuitionistic modal logic (with G.
Bierman) Abstract of a contributed paper in the Logic Colloquium 1994,
The Bulletin of Symbolic Logic, vol 1(2), June 1995.
- A New Proof System for Intuitionistic Logic (with L.
C. Pereira) The Bulletin of Symbolic Logic, vol 1(1):101, 1995
From a Logical Perspective I. (with Benton and Bierman)
University of Cambridge Computer Laboratory Technical Report 365.
for Intuitionistic Linear Logic. (with Nesi and Ritter).
Proceedings of the Workshop on
Higher Order Algebra, Logic and Term Rewriting, HOA'93. In Volume 816
of Lecture Notes in Computer Science, Springer Verlag. 1994
- The ACQUILEX LKB: An Introduction
(with Copestake, Sanfilippo and Briscoe). In "Inheritance, Defaults and
the Lexicon". Eds. Ted Briscoe,
Valeria de Paiva and Ann Copestake. Studies in Natural Language
- Types and Constraints in the LKB . In "Inheritance,
Defaults and the Lexicon". Eds. Ted
Valeria de Paiva and Ann Copestake. Studies in Natural Language
Intuitionistic Linear Logic
(extended abstract). (with Martin Hyland).
Annals of Pure and Applied Logic, 64(3), pp.273-291, 1993. pdf
Calculus for Intuitionistic Linear Logic. (with Benton,
Bierman and Hyland). Proceedings of the First International
Conference on Typed Lambda Calculus. In Volume 664 of Lecture Notes in
Computer Science, Springer Verlag. 1993
and Categorical Models Revisited. (with
Benton, Bierman and Hyland). Proceedings of Sixth Conference on
Computer Science Logic. In Volume 702 of Lecture Notes in Computer
Science, Springer Verlag. 1993
- Intuitionistic Necessity Revisited (extended abstract).
(with Bierman). In Proceedings of Applied Logic Conference, December
1992. Second version in PRATICA: Proofs, Types and
Categories, edited by Hermann Hausler and Luiz Carlos Pereira,
for Intuitionistic Linear Logic. (with Benton,
Bierman and Hyland). Technical Report 262, University of Cambridge
Computer Laboratory. August 1992.
(with J.M.E. Hyland) In "O que nos faz
Special number in Logic of "Cadernos do Dept. de Filosofia da PUC",
Pontificial Catholic University of Rio de Janeiro, Abril 1991.
Model of Linear Logic.In Proceedings
of Category Theory and Computer Science, Manchester, UK, September
1989. Springer-Verlag LNCS 389 (eds. D. Pitt, D. Rydeheard, P. Dybjer,
A. Pitts and A. Poigne).
Dialectica Categories. In
Proc of Categories in Computer Science and Logic, Boulder, CO,
1987. Contemporary Mathematics, vol 92, American Mathematical Society,
1989 (eds. J. Gray and A. Scedrov)
Drafts, Technical Reports and Loose Ends
I am collecting here some manuscripts on subjects that I would like
to come back to. Comments (and mistakes, typos, omissions, etc.)
Theory and Linear Logic. Preliminary notes
for a lecture course. This course was taught four times:
first at PUC-RJ, Brazil, then as a graduate course in the Computer Lab,
Cambridge, then at the European Summer School on Language, Logic and
Information (ESLLI), in Prague (1996) and finally at School of Computer
Science, Birmingham, UK (1997).
and Applications R. Crouch, Josef van
Genabith, V. de Paiva and E. Ritter (editors) Dagstuhl-Seminar-Report,
248, IBFI gem GmbH, Schloss Dagstuhl, D-66687 Wadern, Germany, ISSN
- Mini-colloquium on Linear Logic for Natural Language
Dick Crouch, Josef van Genabith, Mark Hepple and Valeria de Paiva.
School of Computer Science, University of Birmingham, B15 2TT, School
of Computer Science Technical Reports, CSR-97-6, May 1997.
Model of the Lambek
Calculus. This paper was presented at the Amsterdam
Colloquium, 1990. I believe the version here is identical to the one in
the proceedings, but I'm not absolutely sure.
- Cut-elimination for Full Intuitionistic Linear
Logic (with Torben Brauner) Technical Report 395, University
of Cambridge, Computer Laboratory, May 1996.
- Proceedings of the ACQUILEX Workshop on Default
the Lexicon. Ted Briscoe, Ann Copestake and Valeria de Paiva
Technical Report 238 from Computer Laboratory, University of Cambridge.
- A Linear Specification Language
for Petri Nets. (with C.
Brown and D. Gurr) Technical Report 363 from Computer Science
Department, University of Aarhus, Denmark, October 1991.
Logic and Petri Nets. Technical Report 225 from Computer
Laboratory, University of Cambridge. June 1991.
Technical Report 213 from Computer Laboratory, University of Cambridge.
- Subtyping in Ponder. Technical Report 203 from
Computer Laboratory, University of Cambridge.
of a State Oriented
version of Linear Logic by Alex Tucker, ex Ph. D student,