
Dialectica Categories for the Lambek CalculusIn 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 ofcourse modality !, as Girard did, to reintroduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also…Read more

26Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a wellestablished method for measuring their performance. However, the availability of such libraries for nonclassical 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 LogicsIn Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 3552. 2000.

19An ecumenical notion of entailmentSynthese 123. 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

7Dialectica categories, cardinalities of the continuum and combinatorics of idealsLogic Journal of the IGPL 25 (4): 585603. 2017.

2Relating Categorical and Kripke Semantics for Intuitionistic Modal LogicsIn Michael Zakharyaschev, Krister Segerberg, Maarten de Rijke & Heinrich Wansing (eds.), Advances in Modal Logic, Volume 2, Csli Publications. pp. 3552. 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 typetheoretic and categorytheoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show …Read more

87On an intuitionistic modal logicStudia Logica 65 (3): 383416. 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

17Intuitionistic hybrid logicJournal of Applied Logic 4 (3): 231255. 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 wellmotivated version of intuitionistic hybrid logic and prove essential prooftheoretical results for a natural deduction formulation of it. Our…Read more

4Linear explicit substitutionsLogic Journal of the IGPL 8 (1): 731. 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 nontrivial interactions between linearity and explicit substitutions and t…Read more

4On an Intuitionistic Modal LogicStudia 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

77LinealesO Que Nos Faz Pensar 107123. 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 toystructure a not distant cousin of a toylanguage. 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

61Elements of Categorical Logic: Fifty Years Later (review)Logica Universalis 7 (3): 265273. 2013.

79A short note on intuitionistic propositional logic with multiple conclusionsManuscrito 28 (2): 317329. 2005.A common misconception among logicians is to think that intuitionism is necessarily tiedup 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

29Full intuitionistic linear logicAnnals of Pure and Applied Logic 64 (3): 273291. 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 prooftheoretic problem arises from the observation of Schellinx that cut elimin…Read more

University of BirminghamResearcher
Cupertino, CA, United States of America
Areas of Specialization
Logic and Philosophy of Logic 
Science, Logic, and Mathematics 