• G. Bellin.
  ``Mechanizing Proof Theory.
  Resource-Aware Logics and Proof Transformation
  to Extract Implicit Information''.
  Ph.D. thesis, Department of Philosophy, Stanford University, June 1990

Classical Logic

• G.Bellin, M.Hyland, E.Robinson and C.Urban.
  "Categorical Proof Theory of Classical Propositional Calculus"
  Theoretical Computer Science - Vol. 364, 2, November 2006, pp. 146-165.
  ps file | pdf file

Logic for Pragmatics

• A talk at CSLI On logics of abstract illocutionary forces Stanford, 6 june 2011.

• G. Bellin
  "Assertions, hypotheses, conjectures, expectations: Rough-set semantics and proof-theory",
  final version of the paper for the Proceedings of the Natural Deduction Conference, Rio de Janeiro, July 2-6, 2001
  last revision April 2011.
  pdf file
  

• G. Bellin
  "A Term Assignment for Dual Intuitionistic Logic",
  conference paper presented at the LICS'05-IMLA'05 Workshop, Chicago, IL, June 30, 2005
  ps file | pdf file
  

• G. Bellin
  "Natural Deduction and term assignment for co-Heyting algebras in Polarized Bi-Intuitionistic Logic",
  Submitted to the Proceedings of the Natural Deduction Conference, Rio de Janeiro, July 2-6, 2001
  (revised summer 2004)
  ps file | pdf file
  

• G. Bellin and Corrado Biasi
  "Towards a logic for pragmatics: Assertions and conjectures",
  In: Journal of Logic and Computation Special Issue with the Proceedings of the Workshop on
  Intuitionistic Modal Logic and Application (IMLA-FLOC 2002), V.de Paiva, R.Gore' and M. Mendler eds.,
  Volume 14, Number 4, 2004, pp. 473-506.
  ps file | pdf file
  

• G. Bellin.
  "Towards a formal pragmatics:
  an intuitionistic theory of assertive and conjectural judgements with an extension of Goedel, McKinsey and Tarski's S4 translation"
  conference paper presented at the IMLA-FLOC'02 workshop, Copenhagen, 2002.
  ps file | pdf file
  

• G. Bellin and Corrado Biasi.
  "Cut-Elimination for the logic of pragmatics"
  (This is work in progress, which summarizes dr Corrado Biasi's Tesi di Laurea.
  It substantially refines and develops the ideas and the direction of research
  presented at the IMLA-FLOC'02 conference.)
  ps file | pdf file

• G. Bellin and Kurt Ranalter.
  "A Kripke-style semantics for the intuitionistic logic of pragmatics ILP"
  "Journal of Logic and Computation", vol. 13, n. 5, 2003, pp.755-775
  special issue for the Dagstuhl Seminar n. 01141
  on Semantic Foundations of Proof-search, 1-6 April 2001,
  ps file | pdf file

• G. Bellin and Carlo Dalla Pozza.
  A pragmatic interpretation of substructural logics
  in Reflections on the Foundations of Mathematics, Essays in Honor of Solomon Feferman,
  W.Sieg, R.Sommer and C.Talcott eds. ASL Lecture Notes in Logic ; 15, 2002.
  ps file | pdf file

Linear Logic

• G. Bellin.
  ``Chu's Construction: A Proof-theoretic Approach''
  in Ruy J.G.B. de Queiroz editor, "Logic for Concurrency and Synchronisation", Kluwer Trends in Logic n.18, 2003, pp.93-114.
  (Submitted April 1999, revised July 2000).
  Copyright 2001 Kluwer Academic Publishers. All rights reserved.
  dvi file | ps file

• G. Bellin.
  ``Two paradigms of logical computation in Affine Logic?''
  in Ruy J.G.B. de Queiroz editor, "Logic for Concurrency and Synchronisation", Kluwer Trends in Logic n.18, 2003, pp.115-150.
  (Submitted October 1999, revised June 2001).
  Copyright 2001 Kluwer Academic Publishers. All rights reserved.
  dvi file | ps file

• G. Bellin and A. Fleury.
  ``Planar and Braided Proof-nets for MLL with Mix''
  Archive for Mathematical Logic 1998, 37, pp.309-325.
  dvi file | ps file

• G. Bellin.
  ``Subnets of Proof-nets in multiplicative linear logic with MIX''
  Mathematical Structures in Computer Science vol.7, pp.663-699 (1997).
  Copyright Cambridge University Press 1997
  dvi file | ps file

• G. Bellin and J. van de Wiele.
  ``Subnets of Proof-nets in MLL-''
  in: Advances in Linear Logic J-Y. Girard, Y. Lafont and L. Regnier eds.
  London Mathematical Society Lecture Note Series 222, 1995
  Copyright Cambridge University Press 1995
  dvi file | ps file

• G. Bellin.
  ``Proof Nets for Multiplicative and Additive Linear Logic''
  Technical Report LFCS-91-161
  Department of Computer Science, University of Edinburgh, May 1991
  dvi file | ps file

• G. Bellin, Valeria de Paiva and Eike Ritter.
  ``Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic''
  paper presented at the conference Methods for Modalities 2,
  Institute for Logic, Language and Computation, University of Amsterdam, November 29-30, 2001.
  ps file

• G. Bellin.
  ``Ramsey Interpreted: A Parametric Version of Ramsey's Theorem''
  in: Logic and Computation: Proceedings of a Symposium held at Carnegie-Mellon University
  Contemporary Mathematics 106, AMS, 1990, pp. 17-37.
  

• G. Bellin.
  ``A system of natural deduction for GL''
  in: Teoria LI, 2 1985, pp. 89-114. pdf file
  

• G. Bellin.
  ``Herbrand's Theorem for Calculi of Sequents LK and LJ''
  in: Proceedings of the Fifth Scandinavian Logic Symposium
  Aalborg University Press, 1979, pp. 285-300.

• G. Bellin.
  Linear Logic (Philosophical issues in)
  article commissioned for the Routledge Encyclopedia of Philosophy, 1995
  (in the end, the mathematician Gavin Bierman did the job).

• G. Bellin.
  ``On the Pi-calculus and distributed calculi for co-intuitionistic logic''
  pdf file
  Paper accepted at LAM'11, (Logics, Agents and Mobility), CONCUR 2011, Aachen, Germany, 10 Sept 2011.

• G. Bellin and P.J.Scott.
  ``On the Pi-calculus and linear logic''
  in: Theoretical Computer Science 135 (1994) 11-65
  Copyright 1994 - Elsevier Science Publishers B.V. All rights reserved
  dvi file | ps file

• G. Bellin and J. Ketonen.
  ``A decision procedure revisited: Notes on direct logic, linear logic and its implementation''
  in: Theoretical Computer Science 95 (1992) 115-142
  Copyright 1992 - Elsevier Science Publishers B.V. All rights reserved
  dvi file

• G. Bellin and J. Ketonen.
  ``Experiments in Automatic Theorem Proving''
  Technical Report No. STAN-CS-87-1155
  

back home