
Selected publications
Books
Published papers
Preliminary versions are available online. Please refer to the printed publication
for the final version.
 Light Logics and HigherOrder Processes, with
U. Dal Lago and D. Sangiorgi, Mathematical Structures in Computer Science, vol. 26(6) (2016) 969992 (Cambridge University Press, Cambridge, UK).
A shorter version appeared on
Expressiveness in Concurrency, EXPRESS 2010, EPTCS, 41, 2010, pp. 4660.
 Types in Programming Languages, between Modelling, Abstraction, and Correctness, CiE 2016: Pursuit of the Universal, LNCS 9709, 164169, 2016.
 Several types of types in programming languages, History and Philosophy of Computing, HAPOC 2015, IFIP Advances in Information and Communication Technology 487, 216227, Springer 2016.
 On Constructor Rewrite Systems
and the LambdaCalculus,
with
U. Dal Lago. Logical Methods in Computer Science, Vol. 8(3:12), 2012, pp. 127.
A shorter version appeared on ICALP 2009.
36th International Colloquium on
Automata, Languages and
Programming, Track B,
Albers et al. (Eds), Springer LNCS 5556, pp. 163174, July 2009.
 Lingua Universalis.
Annali della Pubblica Istruzione, n. 45, 2011, pp. 6570.
 General Ramified Recurrence is Sound for Polynomial Time
with
U. Dal Lago and M. Zorzi.
Developments in Implicit Computational complExity, DICE 2010, EPTCS, Vol. 23, 4762, May 2010.
 Derivational Complexity is an Invariant Cost Model
with
U. Dal Lago.
FOPARA 2009, Springer LNCS 6324, 88101, 2010.

M. Kaminski, S. Martini (eds),
Computer Science Logic 2008,
Springer LNCS 5213, 2008.
A selection of papers appeared later on ACM Trans. on Comp. Logic (ToCL), Vol. 11(4), 2010.
 Proofs as efficient programs,
with
U. Dal Lago. January 2008. In Deduction, Computation, Experiment,
R. Lupacchini, G. Corsi (Eds.), SpringerVerlag, 2008.
 Elogio di Babele.
Mondo Digitale, no. 2  giugno 2008, 1723.
 Informatica: Elogio di Babele.
January 2008. In Studi offerti a Alessandro Perutelli,
A. Audano et al. (Eds.), Aracne editrice, 2008.
 The weak lambdacalculus as a reasonable machine,
with
U. Dal Lago. May 2007. In Theoretical Computer Science, vol 398(13) (2008) pp. 3250.
(Revised and expanded version of LNCS 3988, pp. 105  114.)
 An invariant cost model for the lambda calculus,
with
U. Dal Lago. November 2005. Available on arxiv.org.
A shorter version appeared on Logical Approaches to Computational Barriers (CiE 2006),
Beckmann et al. (eds), Springer LNCS 3988, pp. 105  114, June 2006.

Optimizing optimal reduction.
A type inference algorithm for elementary affine logic,
with
P. Coppola. ACM Transactions on Computational Logic, vol 7 (2006) pp. 219  260.

(Optimal) duplication is not elementary recursive (journal version),
with A. Asperti and
P. Coppola. Information and Computation,
vol. 193/1 (2004) pp. 2156.
A
preliminary version
appeared in
27th ACM Conference on Principles of Programming Languages,
POPL 2000, Boston, January 2000. ACM Press, New York.

Phase semantics and decidability of elementary affine logic,
with
U. Dal Lago. In Theoretical Computer Science,
vol. 318(3) (2004) pp. 409433.

Higher order linear ramified recurrence,
with U. Dal Lago,
and L. Roversi.
In Types for Proofs and Programs: Third International Workshop,
TYPES 2003,
LNCS 3085, 178193, 2004.

Provando e riprovando, Prefazione al libro
Laboratorio di programmazione in Java di
P. Coppola
e
S. Mizzaro; Apogeo 2004.

Coherence for sharing proofnets (journal version), with
S. Guerrini, and
A. Masini.
In Theoretical Computer Science,
vol. 294(3) (2003) pp. 379409.
A
preliminary version appeared in
RTA96, LNCS 1103, 215229.

Typing lambda terms in elementary logic with linear constraints,
with
P. Coppola.
Conference on Typed
LambdaCalculus and Applications, TLCA01, LNCS 2044, 7690, Springer, Berlin, 2001.
Postscript version is here.

Proof nets, garbage, and computation, (journal version), with
Stefano Guerrini and
Andrea Masini.
In
Theoretical Computer
Science. vol. 253(2) (2001), pp. 185237.
A
preliminary version appeared in
Typed LambdaCalculus and Applications, TLCA97, Springer, Berlin, LNCS 1210,
181195.

Modal logic, linear logic, optimal lambdareduction,with
Stefano Guerrini and
Andrea Masini.
in Logic and Foundations of Mathematics, A. Cantini, E. Casari,
P. Minari eds., Kluwer, Dordrecht, 1999.

An analysis of (linear) exponentials based on extended sequents,
with
Stefano Guerrini and
Andrea Masini.
In
Logic Journal of the IGPL, Vol.6 No. 5, pp. 735753, 1998.
Postscript version is
here.

Experiments in linear natural deduction, with
Andrea Masini. In Theoretical
Computer Science. vol. 176 (1997), 159173.
Postscript version is
here.

Review of
Hyperproof for the Macintosh, by Jon Barwise and John Etchemendy
(CSLI Publications, 1994). In
Hystory and Philosophy of Logic 17:9697, 1996.
Postscript version is
here.

A computational interpretation of modal proofs, with
Andrea Masini,
in
Proof Theory of Modal Logic,
H. Wansing (Ed.), Kluwer, 1996, 213241.
Postscript version is
here.

Review of
Truth and Modality for Knowledge Representation, by R. Turner
(Pitman, London 1990, and The MIT Press, Cambridge,
Mass., 1991).
The Journal of Symbolic Logic 61(2):693696, 1996.
Postscript version is
here.

On the fine structure of the exponential rule, with
Andrea Masini, in
Advances in Linear Logic,
J.Y. Girard, Y. Lafont, L. Regnier (eds), Cambridge University Press,
pages 197210, 1995.
Postscript version is
here.

A modal view of linear logic, with
Andrea Masini.
The Journal of Symbolic Logic, vol 59(1994) no. 3, 888899.
Postscript version is
here.

Prooffunctional connectives and realizability, with
Franco Barbanera.
Archive for Mathematical Logic, vol. 33(1994), 189211.
Postscript version is
here.

E. Boerger, G. Jaeger, H. KleineBuening, S. Martini, M.M. Richter,
Computer Science Logic, Selected papers of CSL'92,
LNCS 702, (SpringerVerlag, Berlin) 1993.

An extension of System F with subtyping, with
Luca Cardelli,
John C. Mitchell,
and
Andre Scedrov.
Digital Eq. Co.
SRC Report 80. Revised version in Information and
Computation vol. 109(1994), 456;
preliminary version in International Conference on
Theoretical Aspects of Computer Software,
LNCS 526, 750770. Postcript version is
here.
