• The Dialectica Categories
    with Vaz De Paiva
     213. 1991.
  •  100
    A common misconception among logicians is to think that intuitionism is necessarily tied-up with single conclusion calculi. Single conclusion calculi can be used to model intuitionism and they are convenient, but by no means are they necessary. This has been shown by such influential textbook authors as Kleene, Takeuti and Dummett, to cite only three. If single conclusions are not necessary, how do we guarantee that only intuitionistic derivations are allowed? Traditionally one insists on restri…Read more
  • Inheritance Defaults (Studies in Natural Language Processing)
    with Edward Briscoe and Ann Copestake
    Cambridge University Press. 1993.
    reissued in soft cover 2006
  • Annie Zaenen’s research has broadly influenced the field of linguistics from the underlying architecture of formal theories to the minute details of lexical representation. This volume assembles a wide range of essays from linguists who have been profoundly influenced by Zaenen’s work. Taking Zaenen as a model, the contributors explore a variety of topics, including the mapping of syntax onto argument and the relationship between syntax and semantics. From Quirky Case to Representing Space prese…Read more
  •  4
    Linguistic Issues in Language Technology (LiLT) is an open-access journal that focuses on the relationships between linguistic insights and language technology. In conjunction with machine learning and statistical techniques, deeper and more sophisticated models of language and speech are needed to make significant progress in both existing and newly emerging areas of computational language analysis. The vast quantity of electronically accessible natural language data (text and speech, annotated…Read more
  • Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the 22nd Workshop on Logic, Language, Information and Computation, WoLLIC 2015, held in the campus of Indiana University, Bloomington, IN, USA in July 2015. The 14 contributed papers, presented together with 8 invited lectures and 4 tutorials, were carefully reviewed and selected from 44 submissions. The focus of the workshop was on interdisciplinary research i…Read more
  • This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science.
  •  231
    Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrapping of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic the…Read more
  • Relating Categorical and Kripke Semantics for Intuitionistic Modal Logics
    with Natasha Alechina and Eike Ritter
    In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 35-52. 1998.
  •  37
    An ecumenical notion of entailment
    Synthese 198 (S22): 5391-5413. 2019.
    Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof th…Read more
  •  13
    Relating Categorical and Kripke Semantics for Intuitionistic Modal Logics
    with Natasha Alechina and Eike Ritter
    In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 35-52. 1998.
    We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show …Read more
  •  18
    Dialectica categories, cardinalities of the continuum and combinatorics of ideals
    with Samuel G. da Silva
    Logic Journal of the IGPL 25 (4): 585-603. 2017.
  •  19
    Intuitionistic N-Graphs
    with M. Quispe-Cruz, A. G. de Oliveira, and R. J. G. B. de Queiroz
    Logic Journal of the IGPL 22 (2): 274-285. 2014.
    The geometric system of deduction called N-Graphs was introduced by de Oliveira in 2001. The proofs in this system are represented by means of digraphs and, while its derivations are mostly based on Gentzen's sequent calculus, the system gets its inspiration from geometrically based systems, such as the Kneales' tables of development, Statman's proofs-as-graphs, Buss' logical flow graphs, and Girard's proof-nets. Given that all these geometric systems appeal to the classical symmetry between pre…Read more
  •  25
    Linear logic model of state revisited
    Logic Journal of the IGPL 22 (5): 791-804. 2014.
    In an unpublished note Reddy introduced an extended intuitionistic linear calculus, called LLMS (for Linear Logic Model of State), to model state manipulation via the notions of sequential composition and ‘regenerative values’. His calculus introduces the connective ‘before’ ▹ and an associated modality †, for the storage of objects sequentially reusable. Earlier and independently de Paiva introduced a (collection of) dialectica categorical models for (classical and intuitionistic) Linear Logic,…Read more
  •  102
    On an intuitionistic modal logic
    with G. M. Bierman
    Studia Logica 65 (3): 383-416. 2000.
    In this paper we consider an intuitionistic variant of the modal logic S4 (which we call IS4). The novelty of this paper is that we place particular importance on the natural deduction formulation of IS4— our formulation has several important metatheoretic properties. In addition, we study models of IS4— not in the framework of Kirpke semantics, but in the more general framework of category theory. This allows not only a more abstract definition of a whole class of models but also a means of mod…Read more
  •  38
    Intuitionistic hybrid logic
    Journal of Applied Logic 4 (3): 231-255. 2006.
    Hybrid logics are a principled generalization of both modal logics and description logics, a standard formalism for knowledge representation. In this paper we give the first constructive version of hybrid logic, thereby showing that it is possible to hybridize constructive modal logics. Alternative systems are discussed, but we fix on a reasonable and well-motivated version of intuitionistic hybrid logic and prove essential proof-theoretical results for a natural deduction formulation of it. Our…Read more
  •  7
    Linear explicit substitutions
    with N. Ghani and E. Ritter
    Logic Journal of the IGPL 8 (1): 7-31. 2000.
    The λσ-calculus adds explicit substitutions to the λ-calculus so as to provide a theoretical framework within which the implementation of functional programming languages can be studied. This paper generalises the λσ-calculus to provide a linear calculus of explicit substitutions, called xDILL, which analogously describes the implementation of linear functional programming languages.Our main observation is that there are non-trivial interactions between linearity and explicit substitutions and t…Read more
  •  10
    On an Intuitionistic Modal Logic
    with G. M. Bierman
    Studia Logica 65 (3). 2000.
    In this paper we consider an intuitionistic variant of the modal logic S4 (which we call IS4). The novelty of this paper is that we place particular importance on the natural deduction formulation of IS4 -- our formulation has several important metatheoretic properties. In addition, we study models of IS4 -- not in the framework of Kripke semantics, but in the more general framework of category theory. This allows not only a more abstract definition of a whole class of models but also a means of…Read more
  •  236
    Lineales
    with Martin Hyland
    O Que Nos Faz Pensar 107-123. 1991.
    The first aim of this note is to describe an algebraic structure, more primitive than lattices and quantales, which corresponds to the intuitionistic flavour of Linear Logic we prefer. This part of the note is a total trivialisation of ideas from category theory and we play with a toy-structure a not distant cousin of a toy-language. The second goal of the note is to show a generic categorical construction, which builds models for Linear Logic, similar to categorical models GC of [deP1990], but …Read more
  •  31
    WOLLIC, CSLI, Stanford, USA July 18–21, 2006
    with Anjolina Grisi de Oliveira, Valéria de Paiva, Eli Ben-Sasson, and Yuri Gurevich
    Bulletin of Symbolic Logic 13 (3). 2007.
  •  158
    The Dialectica Categories
    Dissertation, University of Cambridge, UK. 1990.
    This thesis describes two classes of Dialectica categories. Chapter one introduces dialectica categories based on Goedel's Dialectica interpretation and shows that they constitute a model of Girard's Intuitionistic Linear Logic. Chapter two shows that, with extra assumptions, we can provide a comonad that interprets Girard's !-course modality. Chapter three presents the second class of Dialectica categories, a simplification suggested by Girard, that models (classical) Linear Logic and chapter f…Read more
  •  56
    Full intuitionistic linear logic
    with Martin Hyland
    Annals of Pure and Applied Logic 64 (3): 273-291. 1993.
    In this paper we give a brief treatment of a theory of proofs for a system of Full Intuitionistic Linear Logic. This system is distinct from Classical Linear Logic, but unlike the standard Intuitionistic Linear Logic of Girard and Lafont includes the multiplicative disjunction par. This connective does have an entirely natural interpretation in a variety of categorical models of Intuitionistic Linear Logic. The main proof-theoretic problem arises from the observation of Schellinx that cut elimin…Read more