Thematic list of main publications by Sara Negri
***NOT UPDATED! FOR AN UPDATED LIST OF PUBLICATIONS SEE THIS PAGE***
Proof Analysis: A Contribution to Hilbert's Last Problem (with Jan von Plato), Cambridge University Press, August 2011.
Structural Proof Theory .
Cambridge University Press. Contents.
Connected to the book is an interactive sequent calculus proof
editor that can be found through
Aarne Ranta's home page.
The book has also a web page.
Philosophical logics:

Proofs and countermodels in nonclassical logics.
Logica Universalis, vol. 8, pp. 2560, 2014.
 Proof analysis beyond geometric theories: from rule systems to systems of rules. Journal of Logic and Computation, in press.
 A cutfree sequent system for Grzegorczyk logic with an application
to the GödelMcKinseyTarski embedding. With Roy Dyckhoff, Journal of Logic and Computation,
pdf file.
 Proof analysis in intermediate logics (with Roy Dyckhoff), Archive for Mathematical Logic, vol. 51, pp. 7192, 2012, pdf file .
 Countermodels from Sequent Calculi in MultiModal Logics, with Deepak Garg and Valerio Genovese, proceedings of LICS 2012,
IEEE Computer Society, pp. 315324, 2012,
pdf file,
technical report.
 Proof theory for modal logic, Philosophy Compass, 6/8 (2011), pp. 523538,
pdf file.
 Does the deduction theorem fail for modal logic? (with Raul Hakli), Synthese, vol. 187, pp. 849867, 2012,
pdf file .
 Decidability for Priorean Linear Time using a FixedPoint Labelled Calculus (with Bianca
Boretti), Springer Lecture Notes in Computer Science, vol. 5607, Proceedings of
Tableaux 2009 .
 On the finitization of Priorean linear time (with Bianca
Boretti), in D'Agostino et al. (eds) New Essays in Logic and Philosophy of Science, College Publications, London, 2010,
pdf file .
 Two ways of finitizing linear time (with Bianca Boretti), ms. 2007.
pdf.
 Proof analysis in nonclassical logics,
in "Logic Colloquium '05:
Proceedings of the Annual European Summer Meeting of the Association for
Symbolic Logic, Athens, Greece, July 28August 3, 2005". C. Dimitracopoulos,
L. Newelski, D. Normann, and J. Steel (eds)
ASL Lecture Notes in Logic, vol. 28, pp. 107128,
pdf file
 Proof analysis in modal logic, Journal of Philosophical Logic, vol 34,
pp. 507544, 2005.
pdf file .
 Cut elimination in provability logic,
Mathematisches Forschunginstitut Oberwolfach, Report no. 14/2005, p. 9017.
pdf file.
History and foundations, formal epistemology:
 Meaning in use, with Jan von Plato, in H. Wansing (ed) Dag Prawitz on Proofs and Meaning, Trends in Logic, Springer, in press.
 The ChurchFitch knowability paradox in the light of structural proof theory, with Paolo Maffezioli and Alberto Naibo, Synthese, vol. 190, pp. 26772716, 2013,
pdf file .
 A Gentzenstyle analysis of Public Announcement Logic,
(with Paolo Maffezioli), in X. Arrazola and M. Ponte (eds) Proceedings of the International Workshop on Logic and Philosophy of Knowledge, Communication
and Action, pp. 293313, University of the Basque Country Press, 2010,
pdf file .
 Reasoning about collectively accepted group beliefs (with Raul Hakli), in Herzig, A. and E. Lorini (eds) ``Logical Methods for Social Concepts'' Journal of Philosophical Logic, vol. 40, pp. 531555, 2011.
pdf file .
 Kripke completeness revisited, in G. Primiero and S. Rahman (eds.), "Acts
of Knowledge  History, Philosophy and Logic", College Publications, 2009,
pdf file.
 Proof theory for distributed knowledge (with Raul Hakli), Computational Logic in MultiAgent Systems, Springer Lecture Notes in Artificial Intelligence, vol. 5405, pp. 100116, Springer, 2008,
pdf file.
 The duality of classical and constructive
notions and proofs (with Jan von Plato), in
"From Sets and Types to Topology and Analysis: Towards Practicable Foundations
for Constructive Mathematics" (L. Crosilla, P. Schuster, eds.), Oxford
University Press, , pp. 149161, 2005.
pdf file .
 Hilbertin viimeinen ongelma, (in Finnish) written with Jan von Plato,
Arkhimedes, no. 5, pp. 1720, 2002.
Proof theory and proof systems:

Varieties of linear calculi,
Journal of Philosophical Logic, vol 31, pp. 569590, 2002.
ps,
dvi,
pdf file .

A normalizing system of natural deduction for intuitionistic linear
logic,
Archive for Mathematical Logic,
vol. 41, pp.789810, 2002.
pdf file .
 Sequent calculus in natural deduction style,
written with Jan von Plato,
Abstract,
pdf file .
The Journal of Symbolic Logic, vol. 66, pp. 18031816, 2001.

Admissibility of structural rules for contractionfree systems of
intuitionistic logic,
written with
Roy Dyckhoff, 1998.
Abstract,
pdf file .
.
The Journal of Symbolic Logic, 65, (December 2000), pp. 14991518.

Cut elimination in the presence of axioms,
(written with Jan von Plato),
The Bulletin of Symbolic Logic, vol. 4, pp. 418435, 1998.
Applications of proof theory:
 Decision methods for linearly ordered Heyting algebras
(with Roy Dyckhoff), Archive for Mathematical Logic, vol 45,
pp. 411422, 2006,
pdf file .
 Equality in the presence of apartness:
An application of structural proof analysis to intuitionistic axiomatics
(with Bianca Boretti), in
"Constructivism: Mathematics, Logic, Philosophy and Linguistics"
G. Ronzitti and G. Heinzmann (eds),
Philosophia Scienti?, pp. 6179, Cahier sp?cial 6, 2006.

Permutability of rules for linear lattices ,
in C. Calude and H. Ishihara (eds)
"Constructivity, Computability, and Logic"
Journal of Universal Computer Science, vol 11, no. 12, pp. 19861995, 2005.
pdf file.

Proof systems for lattice theory, written with Jan von Plato,
Mathematical Structures in Computer Science, vol. 14, pp. 507526, 2004.
ps file .

Permutability of rules in lattice theory,
written with Jan von Plato, Algebra Universalis, vol. 48 (2002), pp. 473477.
pdf file .

Contractionfree sequent calculi for geometric theories, with an application to
Barr's theorem,
Archive for Mathematical Logic, vol. 42 (2003), pp. 389401
(earlier version available from
Reports Institut MittagLeffler, Preprint series: Mathematical Logic  2000/2001, No. 22) . Correction note
dvi file.

Proof theoretical analysis of order relations,
written with Jan von Plato and Thierry Coquand, Archive
for Mathematical Logic, vol. 43, pp. 297309, 2004.
pdf file .
Also available from
Reports Institut MittagLeffler,
Preprint series: Mathematical Logic  2000/2001, No. 18.
 Five Lectures on Proof Analysis
lecture notes for the tutorial given at the
Summer School on Proof Theory, Computation and Complexity, Dresden 2003.

Admissibility of structural rules for extensions of contractionfree sequent calculi,
written with
Roy Dyckhoff, Logic Journal of the IGPL,
vol. 9, no. 4, 2001 .
pdf file .

Conservativity of apartness over
equality, revisited,
Research Report CS/99/4, Computer Science Department, University
of St. Andrews, 1999.
compressed dvi file .
 A sequent calculus for constructive ordered fields.
Abstract.
In "Reuniting the antipodes,
Constructive and Nonstandard Views of the Continuum", P. Schuster et al. eds,
pp. 143155, Kluwer, Dordrecht, 2001.
pdf file .
 Sequent calculus proof theory of intuitionistic apartness and
order relations, Archive for Mathematical Logic,
vol. 38, no. 8, pp. 521547, 1999.
Abstract,
pdf file .
Continuous lattices and integration:

Continuous domains as formal spaces , Mathematical Structures in
Computer Science, vol. 12, pp. 1952, 2002. Correction note
dvi file.

Continuous lattices in formal topology, 1997.
In Lecture Notes in Computer Science, E. Gimenez and
C. Paulin (eds), selected papers of the Types meeting, Aussois, 1996,
LNCS 1512, pp. 333353, Springer, 1998.
Full article just rescued (on 13.1.2009) from my old PowerBook!

The generalized Riemann integral
on locally compact spaces , written
with Abbas Edalat. Topology and its Applications,
vol. 89, pp. 121150, 1998.
Abstract,
dvi.gz file .

The generalized Riemann integral
on locally compact spaces (extended abstract), written
with Abbas Edalat, in ``Advances in Theory and Formal
Methods of Computing'', A. Edalat, S. Jourdan
and G. McCusker (eds), Imperial College Press, London, pp. 7384, 1996.
Pointfree topology and analysis:
 Decidability of positivity under Stone compactification, note, 1997.
Abstract,
ps.gz file.
 Dalla Topologia Formale all'Analisi (Ph.D. thesis, in Italian),
Dept. of Pure and Applied Mathematics, University of Padova, 1996.
 The HahnBanach Theorem in Type
Theory, written with Jan Cederquist and Thierry Coquand,
to appear in ``TwentyFive Years of Constructive
Type Theory'', G. Sambin and J. Smith (eds), Oxford University Press.
Abstract,
dvi.gz file .
 A constructive proof of
the HeineBorel covering theorem for formal reals , written with
Jan Cederquist, in ``Types for
Proofs and Programs'', S. Berardi and M. Coppo (eds), Lecture Notes in
Computer Science 1158, pp. 6275, Springer Verlag, 1996.
Abstract,
ps.gz file ..

The continuum as a formal space, written
with Daniele Soravia,
Archive for Mathematical Logic,
vol. 38, no. 7, pp. 423447, 1999.
Summary ,
ps file .

Tychonoff's theorem in the framework
of formal topologies , written with Silvio Valentini,
The Journal of Symbolic Logic, 62,4, pp. 13151332, 1997.
You can see a summary
here .
 Stone bases, alias the constructive content of Stone
representation ( ps ,
dvi),
in ``Logic and Algebra'', A. Ursini and
P. Agliano' (eds), Dekker, New York, pp. 617636, 1996.
Algebraic and topological models:
 From Kripke Models to Algebraic Countervaluations,
written with Jan von Plato, 1997.
Abstract.
In "
Tableaux '98",
Automated Reasoning with Analytic Tableaux
and related methods, Harrie de Swart ed., LNAI 1397, pp. 247.270,
1998,
pdf file .

Semantical observations on the
embedding of Intuitionistic Logic into Intuitionistic Linear Logic
( ps.gz ),
Mathematical Structures in Computer Science, vol. 5, pp. 4168,
Cambridge University Press, 1995.
You can see a summary
here .
Back to Sara's homepage.
Last modified March 2014