Side Projects

Publications

  • Categorical Semantics of Linear Logic for All, Manuscript, submitted 2006.
  • Valeria de Paiva, Eike Ritter, Basic Constructive Modal Logic.
  • Logic without Frontiers:Festschrift for Walter Alexandre Carnielli on the occasion of his 60th Birthday.
    Jean-Yves Béziau and Marcelo Esteban Coniglio (eds.) Volume 17 of Tribute Series, College Publications. London, 2011.
    ISBN 978-1-84890-055-4
  • de Paiva, Valeria, and Alexandre Rademaker. 2012. “Revisiting a Brazilian WordNet”. In Proceedings of Global Wordnet Conference. Matsue: Global Wordnet Association.
  • Valeria de Paiva, Brigitte Pientka: Intuitionistic Modal Logic and Applications (IMLA 2008). Inf. Comput. 209(12): 1435-1436 (2011).
  • Valeria de Paiva , Eike Ritter, Basic Constructive Modality in Jean-Yves Beziau and Marcelo Coniglio (eds)
    Logic without Frontiers, Festschrift for Walter Alexandre Carnielli on the occasion of his 60th birthday, 2011.
  • Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2011. “Intuitionistic Description Logic and Legal Reasoning”. In XVI The Brazilian Logic Conference. Petrópolis, Brazil.
  • Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2011. “Intuitionistic Description Logic and Legal Reasoning”. In 2011 Database and Expert Systems Applications, DEXA, International Workshops. Toulouse: IEEE Computer Society. doi:10.1109/DEXA.2011.46.
  • de Paiva, Valeria, Edward Hermann Haeusler, and Alexandre Rademaker. 2011. “Constructive Description Logics Hybrid-Style”. Electronic Notes In Theoretical Computer Science 273: 21–31.
  • Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2010. “Using Intuitionistic Logic As a Basis For Legal Ontologies”. In Proceedings of the 4th Workshop On Legal Ontologies and Artificial Intelligence Techniques. Fiesole (Florence): European University Institute.
  • Haeusler, Edward Hermann, Valeria de Paiva, and Alexandre Rademaker. 2010. “Using Intuitionistic Logic As a Basis For Legal Ontologies”. Informatica E Diritto (Journal On Informatics and Law) 1: 289–298.
  • 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, Brazil, 2010.
  •  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 information: 10.1016/j.ic.2009.03.006
  • Context Inducing Nouns, (with Charlotte Price and Tracy H. King), To appear  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), to appear 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. (with Olga Gurevich, Richard S. Crouch, Tracy H. King) J. Log. Comput. 18(3): 385-404 (2008).
  • Textual Inference Logic: Take Two, (with D. G. Bobrow, C. Condoravdi, R. Crouch,  L. Karttunen, T. H. King, R. Nairn and A. Zaenen)  Proceedings of the Workshop on Contexts and Ontologies, Representation and Reasoning, CONTEXT 2007.
  • Precision-focused Textual Inference (with Bobrow, D. G., C. Condoravdi, L. Karttunen, T. H. King, L. Price, R. Nairn, L.Price, A. Zaenen) Proceedings of ACL-PASCAL Workshop on Textual Entailment and Paraphrasing, pp. 16-21, 2007.
  • Constructive 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.

  • 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.
  • Modalities in Constructive Logics 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 Michael Mendler.
  • Logics of Context and Modal Type Theories. Mathematical Foundantions of Programming Semantics (Talk); 2004 May; Pittsburgh; PA; USA.
  • Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic (with G. Bellin and E. Ritter), In Methods for Modalities 2001, Amsterdam, November 2001.
  • Preventing Existence (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 paper).
  • Categorical and 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 and their models) Invited talk. Logic, Language and Computation (10th LLC); 2001 May 26; Stanford, CA.
  • Abstract algebraic substructural logics (talk). Stanford University/Computer Science Dept. Theory Lunch; 2001 May 24; Stanford, CA.
  • On an Intuitionistic Modal Logic (with Gavin Bierman), Studia Logica (65):383-416, 2000.
  • Linear Explicit Substitutions (with Neil Ghani and Eike Ritter), in the Journal of the IGPL, vol 8, Issue 1, January 2000, 7-31.
  • Categorical Models 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.
  • Explicit Substitutions for Linear Logical Frameworks (with Iliano Cervesato and Eike Ritter), Proc. Workshop on Logical Frameworks and Meta-Languages, September 1999.
  • Variations on Linear PCF (with Eike Ritter), Proc. WESTAPP-99, 1999.
  • Building Models 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. Pereira, 1999.
  • Categorical Models of Explicit Substitutions (with Neil Ghani and Eike Ritter), Proc FOSSACS-99, LNCS 1578, Springer-Verlag, 1999.
  • Relating Categorical 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.
  • Explicit Substitutions for Constructive 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.
  • Linear Explicit Substitutions (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.
  • Computational Types 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.
  • On 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.
  • Intuitionistic Necessity Revisited. (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.)
  • Cut-Elimination for Full Intuitionistic Linear Logic. (with Brauner). Technical Report 395 from Computer Laboratory, University of Cambridge and BRICS, Denmark. May 1996.
  • A Dialectica Model of State. (with Correa and Haeusler). In CATS'96, Computing: The Australian Theory Symposium Proceedings, Melbourne, Australia, January 1996.
  • Linear 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 (abstract).
  • Computational Types From a Logical Perspective I. (with Benton and Bierman) University of Cambridge Computer Laboratory Technical Report 365. May 1995.
  • Rewriting Properties of Combinators 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 Processing, 1993.
  • Types and Constraints in the LKB . In "Inheritance, Defaults and the Lexicon". Eds. Ted Briscoe, Valeria de Paiva and Ann Copestake. Studies in Natural Language Processing, 1993.
  • Full Intuitionistic Linear Logic (extended abstract). (with Martin Hyland). Annals of Pure and Applied Logic, 64(3), pp.273-291, 1993. pdf
  • A Term 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
  • Linear lambda-calculus 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, 1999.
  • Term Assignment for Intuitionistic Linear Logic. (with Benton, Bierman and Hyland). Technical Report 262, University of Cambridge Computer Laboratory. August 1992.
  • Lineales. (with J.M.E. Hyland) In "O que nos faz pensar" Special number in Logic of "Cadernos do Dept. de Filosofia da PUC", Pontificial Catholic University of Rio de Janeiro, Abril 1991.
  • A Dialectica-like 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).
  • The 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)

Book

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.) gratefully received.
  • Categorical Proof 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).
  • Linear Logic 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 0940-1121, 22.08.99-27.08.99.
  • 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.
  • A Dialectica 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 Inheritance in the Lexicon. Ted Briscoe, Ann Copestake and Valeria de Paiva Technical Report 238 from Computer Laboratory, University of Cambridge. October 1991.
  • 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.
  • Categorical Multirelations, Linear Logic and Petri Nets. Technical Report 225 from Computer Laboratory, University of Cambridge. June 1991.
  • The Dialectica Categories. Technical Report 213 from Computer Laboratory, University of Cambridge. January 1991.
  • Subtyping in Ponder. Technical Report 203 from Computer Laboratory, University of Cambridge. August 1990.
  • Categorical Modelling of a State Oriented version of Linear Logic by Alex Tucker, ex Ph. D student, 1998.
Comments