Thematic list of publications by Sara Negri
In the list that follows, to avoid duplications, publications are grouped according to their main topic; in each group, items are in reverse chronological order; electronic versions of articles available here may differ from the published versions.
Constructive topology and analysis; formal topology

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

The HahnBanach Theorem in Type
Theory, with Jan Cederquist and Thierry Coquand,
in ``TwentyFive Years of Constructive
Type Theory'', G. Sambin and J. Smith (eds), pp. 5772, 1998, Oxford University Press.
Abstract,
dvi.gz file .

A constructive proof of
the HeineBorel covering theorem for formal reals , 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 .

Tychonoff's theorem in the framework
of formal topologies , with Silvio Valentini,
The Journal of Symbolic Logic, 62,4, pp. 13151332, 1997.
You can see a summary
here .

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

Stone bases, alias the constructive content of Stone
representation ( ps ,
dvi),
pdf),
in ``Logic and Algebra'', A. Ursini and
P. Agliano' (eds), Dekker, New York, pp. 617636, 1996.
 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,
ps file.
Structural proof theory
 Le direzioni della ricerca logica in Italia: Teoria strutturale della dimostrazione. In H. Hosni, G. Lolli, and C. Toffalori (eds) "Le direzioni della ricerca logica in Italia". Edizioni della Normale, Pisa, pp. 221253, 2015,
pdf file.
 Proof analysis beyond geometric theories: from rule systems to systems of rules. Journal of Logic and Computation, vol. 27, pp. 513537, 2016
pdf file.

The geometry of proof analysis: from rule systems to systems of rules, Mathematisches Forschunginstitut Oberwolfach, Report no. 52/2011
DOI: 10.4171/OWR/2011/52, pp. 2628.
 A survey of labelled sequent systems (abstract of plenary talk), in F. Ferreira
et al. (eds), Programs, Proofs, Processes, 6th conference on Computability in
Europe, CiE 2010, Dept. of Mathematics, Univ. of Azores, pp. 1516.

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

Sequent calculus in natural deduction style,
with Jan von Plato,
Abstract,
pdf file .
The Journal of Symbolic Logic, vol. 66, pp. 18031816, 2001.

Structural Proof Theory , with Jan von Plato, 274 pp.,
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.

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

Cut elimination in the presence of axioms,
with Jan von Plato,
The Bulletin of Symbolic Logic, vol. 4, pp. 418435, 1998,
pdf file .
Proof Analysis
 From mathematical axioms to mathematical rules of proof: recent developments in proof analysis (with Jan von Plato). Philosophical Transactions of the Royal Society A, in press.

Proof Analysis: A Contribution to Hilbert's Last Problem, with Jan von Plato, 278 pp., Cambridge University Press, August 2011.

Five Lectures on Proof Analysis
lecture notes for the tutorial given at the
Summer School on Proof Theory, Computation and Complexity, Dresden 2003.

Proof theoretical analysis of order relations,
with with Jan von Plato and Thierry Coquand, Archive
for Mathematical Logic, vol. 43, pp. 297309, 2004.
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 .
Algebraic logic, lattice theory, domain theory

Decision methods for linearly ordered Heyting algebras
(with Roy Dyckhoff), Archive for Mathematical Logic, vol 45,
pp. 411422, 2006,
pdf file .

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, with Jan von Plato,
Mathematical Structures in Computer Science, vol. 14, pp. 507526, 2004.
ps file .

Permutability of rules in lattice theory,
with Jan von Plato, Algebra Universalis, vol. 48 (2002), pp. 473477.
pdf 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 .

From Kripke Models to Algebraic Countervaluations,
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 .

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!
Constructive content of classical proofs
 Commentary on Grigori Mints'
``Classical and Intuitionistic Geometric Logic'', with Roy Dyckhoff. IfCoLog Journal of Logics and their Applications, Mints' memorial issue, vol. 4(4), May 2017, pp. 12351239.
 Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, vol. 55, pp 461473, 2016, pdf file.
 Geometrization of firstorder logic, with Roy Dyckhoff.
The Bulletin of Symbolic Logic , vol. 21, pp. 123163, 2015,
pdf file.
 Contractionfree sequent calculi for geometric theories, with an application to Barr's theorem,
Archive for Mathematical Logic, vol. 42 (2003), pp. 389401.
pdf file, Correction note
dvi 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 .
Modal and provability logic
 Proof theory for quantified monotone modal logics (with Eugenio Orlandelli). IfCoLog Journal of Logics and their Applications, in press.
 Nonnormal modal logics: bineighbourhood semantics and its labelled calculi
(with Tiziano Dalmonte and Nicola Olivetti). Advances in Modal Logic 2018, pdf of final version.
 Proof theory for nonnormal modal logics:
The neighbourhood formalism and basic results,
IfCoLog Journal of Logics and their Applications, Mints' memorial issue, vol. 4(4), May 2017, pp. 12411286.

A cutfree sequent system for Grzegorczyk logic with an application
to the GödelMcKinseyTarski embedding, with Roy Dyckhoff, Journal of Logic and Computation, vol. 26, pp. 169187, 2016
pdf file.
 Nonnormal modal logics:
a challenge to proof theory. In In P. Arazim and T. Lavicka (eds) The Logica Yearbook 2016, pp. 125140, College Publications, pdf of final version.
 Recent advances in proof systems for modal logic (abstract of invited talk), In R. Gore' et al. (eds) Advances in Modal Logic , pp. 421422, College Publications, 2014
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 .
 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.
Conditional logic

Counterfactual logic: labelled and internal calculi, two sides of the same coin?
(with Marianna Girlando and Nicola Olivetti). Advances in Modal Logic 2018, pdf of final version.
 A system of proof for Lewis counterfactual, with G. Sbardolini. In L. Felline et al. (eds) New Directions in Logic and the Philosophy of Science, pp. 189203, College Publications, 2016.
 The logic of conditional beliefs: neighbourhood semantics and sequent calculus, with M. Girlando, N. Olivetti, and V. Risch, AiML 2016,
pdf file.
 A sequent calculus for preferential conditional logic based on
neighbourhood semantics, with Nicola Olivetti. Proceedings of Tableaux 2015,
pdf file.
 Proof analysis for Lewis counterfactuals, with Giorgio Sbardolini.
The Review of Symbolic Logic, vol. 9, pp. 4475, 2016, pdf file.
Nonclassical logics

Proofs and countermodels in nonclassical logics.
Logica Universalis, vol. 8, pp. 2560, 2014,
pdf file.

Proof analysis in intermediate logics, with Roy Dyckhoff, Archive for Mathematical Logic, vol. 51, pp. 7192, 2012, pdf file .
 On the duality of proofs and countermodels in labelled sequent calculi (extended abstract of invited talk),
in D. Galmiche and D. Larchey Wendling (eds) Automated Reasoning with Analytic
Tableaux and Related Methods: 22th International Conference, Tableaux 2013, LNAI 8123, Springer,
pdf file.

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 nonclassical logics (abstract of invited talk), Logic Colloquium 2006, Athens, The Bull\
etin of Symbolic Logic, vol. 12, p. 321, 2006.

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 Scientiae, pp. 6179, Cahier special 6, 2006.
 Conservativity of apartness over
equality, revisited,
Research Report CS/99/4, Computer Science Department, University
of St. Andrews, 1999.
compressed dvi file .
Temporal logic
 Decidability for Priorean Linear Time using a FixedPoint Labelled Calculus, with Bianca
Boretti, Lecture Notes in Computer Science, vol. 5607, Proceedings of
Tableaux 2009,
pdf file .

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.
Linear logic

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 .

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 .
Epistemic logic and formal epistemology

Conditional beliefs: from neighbourhood semantics to
sequent calculus,
with Marianna Girlando, Nicola Olivetti, and Vincent Risch. The Review of Symbolic Logic, doi:
10.1017/S1755020318000023, pdf of final version.

Logique Conditionnelle des Croyances, with M. Girlando, N. Olivetti, and V. Risisch. Semantique de Voisinage et Calcul de Sequents, 10 pages, Actes IAF 2016. pdf file.

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 proof theoretical perspective on Public Announcement Logic, with Paolo Maffezioli, Logic and Philosophy of Science, vol. 9, pp. 4959, 2011,
pdf file .

A Gentzenstyle analysis of Public Announcement Logic,
with Paolo Maffeziol, 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 Andreas Herzig and Emiliano Lorini (eds) ``Logical Methods for Social Concepts'' Journal of Philosophical Logic, vol. 40, pp. 531555, 2011.
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 .
Philosophy of mathematics, history and philosophy of logic
 The intensional side of algebraictopological
representation theorems. Synthese, pdf of final version, 2017.
 Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction, with Jan von Plato. In Dieter Probst and Peter Schuster "Concepts of Proof in Mathematics, Philosophy, and Computer Science", Ontos Mathematical Logic. Walter de Gruyter, Berlin, pp. 269290, 2016,
pdf file.
 Meaning in use, with Jan von Plato, in H. Wansing (ed) Dag Prawitz on
Proofs and Meaning, Trends in Logic, Springer, pp. 239257, 2015,
pdf file.
 Kripke completeness revisited, in G. Primiero and S. Rahman (eds.), "Acts
of Knowledge  History, Philosophy and Logic", College Publications, 2009,
pdf file.
Back to Sara's homepage.
Last modified September 2018