• Dialectica Categories for the Lambek Calculus
    In Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2018). 2018.
    We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a κ modality, inspired by Yetter’s work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also…Read more
  •  26
    The ILLTP Library for Intuitionistic Linear Logic
    with Carlos Olarte, Elaine Pimentel, and Giselle Reis
    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. 2000.
  •  19
    An ecumenical notion of entailment
    with Elaine Pimentel and Luiz Carlos Pereira
    Synthese 1-23. forthcoming.
    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
  •  7
    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.
  •  2
    Relating Categorical and Kripke Semantics for Intuitionistic Modal Logics
    with Natasha Alechina and Eike Ritter
    In Michael Zakharyaschev, Krister Segerberg, Maarten de Rijke & Heinrich Wansing (eds.), Advances in Modal Logic, Volume 2, Csli Publications. pp. 35-52. 2000.
    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
  •  17
    Linear logic model of state revisited
    Logic Journal of the IGPL 22 (5): 791-804. 2014.
  •  87
    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
  •  17
    Intuitionistic hybrid logic
    with Torben Braüner
    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
  •  4
    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
  •  4
    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
  •  77
    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
  •  10
    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.
  •  78
    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
  •  5
    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.
  •  31
    The Dialectica Categories
    Dissertation, University of Cambridge, UK. 1990.
  •  29
    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