 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. JeanYves Béziau and Marcelo Esteban Coniglio (eds.) Volume 17 of Tribute Series, College Publications. London, 2011. ISBN 9781848900554 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): 14351436 (2011).
 Valeria de Paiva , Eike Ritter, Basic Constructive Modality in JeanYves 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 HybridStyle”. 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, HybridStyle (V. de Paiva,
H. Hausler e A. Rademaker), in Preproceedings 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 Grammarbased
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.
 Consequenceinformed 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): 385404 (2008).
 An
Institutional View of Categorical Logic and the CurryHowardTait
Isomorphism (with Joseph Goguen, Till Mossakowski, Florian Rabe,
and Lutz Schröder). In Int J Software Informatics, 1 (1), pp.
129–152, 2007.
 PARC's
Bridge 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 2645, 2007.
 Hylo
2007 Proceedings of the Workshop (editor with Patrick Blackburn,
Thomas Bolander,
Torben Brauner,
Joergen Villadsen). Electr.
Notes Theor. Comput. Sci. 174(6): 12 (2007).
 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.
 Precisionfocused
Textual Inference (with Bobrow, D. G.,
C. Condoravdi, L. Karttunen, T. H. King, L. Price, R.
Nairn,
L.Price, A. Zaenen) Proceedings
of ACLPASCAL Workshop on Textual
Entailment and Paraphrasing, pp. 1621, 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.
 Deverbal Nouns in Knowledge Representation
(with O. Gurevich, D. Crouch, and T. H. King), Appeared in
FLAIRS (The Florida Artificial Intelligence Research Society),
May 1113, 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 317329,
juldez, 2005. Word version.
 Preface
of the special volume on Chu Spaces:
theory and applications (with Vaughan Pratt), Theory and
Applications of Categories, Vol. 17, 2006, No.7, pp 19.
 Dialectica
and Chu constructions:
Cousins?Theory and Applications of Categories, Vol. 17,
2006, No. 7, pp 127152.
 A
Parigotstyle Linear Lambdacalculus
for Full
Intuitionistic Linear Logic (with Eike Ritter),Theory and
Applications of Categories, Vol. 17, 2006, No.3, pp 3048.
 Towards
Constructive Hybrid Logic
(Extended Abstract)
(with T. Brauner), Presented at
Methods for Modalities 3, LORIA, Nancy, France, September 2223,
2003. Also appears as a
technical
report from the University of
Roskilde, 2003.
 Full paper from above, submitted with new title Intuitionistic
Hybrid Logic to
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..
 Constructive
CK
for Contexts (with Michael Mendler), In
Proceedings of the Worskhop on Context Representation and Reasoning,
Paris, France, July
2005.
 A
Basic 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.
 Constructive
CK for Contexts
(with Michael Mendler),
Abstract in the ASL Meeting in Stanford, March 2005.
 Equivalence
of Logics: the categorical
proof theory perspective
Abstract of an Invited Talk at Universal Logic, March 2005.
 Relating
Algebraic Models of
Intuitionistic Predicate Logic (with Milly Maietti)
Abstract of talk presented at Universal Logic 2005.
 Relating
Categorical Semantics for
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):136, 2005.
 Towards constructive description logics. Talk at the Workshop on
Intuitionistic
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.
 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.
 Posetvalued
sets, or, How to build models for
Linear Logic
(with Andrea Schalk), Theoretical Computer Science 315 (2004) 83107,
(submitted 1998).
 Natural
Deduction 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
2003.
 Entailment,
Intensionality and Text
Understanding (with Cleo Condoravdi, Richard Crouch, Reinhard
Stolle, Daniel G. Bobrow.) Proceedings Human Language Technology
Conference (HLTNAACL2003), Workshop on Text Meaning, Edmonton,
Canada, May 2003.
 Knowledge
Tracking:
Answering Implicit
Questions. (with Reinhard Stolle, Daniel Bobrow, Cleo
Condoravdi, Richard Crouch) Proceedings AAAI Spring Symposium on New
Directions in Question Answering, Stanford, California, March 2003.
 Flattened
Semantic Representations
(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).
Technical Report
from the University of Bamberg, Germany, July 2002.
 Normalization
Bounds in Rudimentary Linear
Logic
(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.
 Lineales:
algebras 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. BarkerPlummer, D. Beaver, Johan van Benthem and P.
Scotto di Luzio), 2002.
Original version Lineales:
Algebraic Models of
Linear Logic from a Categorical Perspective.
 Scalability
of 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,
2002.
 Making Ontologies Work for Resolving Redundancies Across
documents
(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.
 Extended
CurryHoward 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):383416, 2000.
 Linear
Explicit Substitutions
(with Neil Ghani and Eike Ritter), in the Journal of the IGPL, vol 8,
Issue 1, January 2000, 731.
 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, SpringerVerlag, vol 1784, April 2000.
 Explicit
Substitutions for Linear Logical Frameworks
(with Iliano Cervesato and Eike Ritter), Proc. Workshop on Logical
Frameworks and MetaLanguages, September 1999.
 Variations
on Linear PCF
(with Eike Ritter), Proc. WESTAPP99, 1999.
 Building
Models of Linear Logic
(with Andrea Schalk), Proc. AMAST99, 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 FOSSACS99, LNCS 1578,
SpringerVerlag, 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 downloadable 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 CSR9802 . 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):177193. March 1998 .
 A Formulation of Linear Logic Based on
DependencyRelations (with Torben Brauner) Proceedings of
Annual Conference of the European Association for Computer Science
Logic, Aarhus, Denmark, LNCS 1414, SpringerVerlag, 1997.
 On
Explicit Substitutions and Names
(with Eike Ritter).
Presented at ICALP'97, LNCS 1256 eds. Degano, Gorrieri and
MarchettiSpaccamela. Also Technical Report CSR975, School of
Computer Science, University of Birmingham. March 1997.
 Intuitionistic
Necessity Revisited.
(with Gavin Bierman).
Technical Report CSRP9610, 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.)
 CutElimination
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.273291, 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
lambdacalculus 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
Dialecticalike Model of Linear Logic.In Proceedings
of Category Theory and Computer Science, Manchester, UK, September
1989. SpringerVerlag 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 PUCRJ, 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) DagstuhlSeminarReport,
248, IBFI gem GmbH, Schloss Dagstuhl, D66687 Wadern, Germany, ISSN
09401121, 22.08.9927.08.99.
 Minicolloquium 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, CSR976, 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.
 Cutelimination 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.

Selection  File type icon  File name  Description  Size  Revision  Time  User 
