|
|
Selected publications
Books
Published papers
Preliminary versions are available on-line. Please refer to the printed publication
for the final version.
- On Constructor Rewrite Systems
and the Lambda-Calculus,
with
U. Dal Lago. May 2009. Available on arxiv.org.
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. 163-174, July 2009.
-
M. Kaminski, S. Martini (eds),
Computer Science Logic 2008,
Springer LNCS 5213, 2008.
- Proofs as efficient programs,
with
U. Dal Lago. January 2008. In Deduction, Computation, Experiment,
R. Lupacchini, G. Corsi (Eds.), Springer-Verlag, 2008.
- Elogio di Babele.
Mondo Digitale, no. 2 - giugno 2008, 17-23.
- Informatica: Elogio di Babele.
January 2008. In Studi offerti a Alessandro Perutelli,
A. Audano et al. (Eds.), Aracne editrice, 2008.
- The weak lambda-calculus as a reasonable machine,
with
U. Dal Lago. May 2007. In Theoretical Computer Science, vol 398(1-3) (2008) pp. 32-50.
(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. 21-56.
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. 409-433.
-
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, 178--193, 2004.
-
Provando e riprovando, Prefazione al libro
Laboratorio di programmazione in Java di
P. Coppola
e
S. Mizzaro; Apogeo 2004.
-
Coherence for sharing proof-nets (journal version), with
S. Guerrini, and
A. Masini.
In Theoretical Computer Science,
vol. 294(3) (2003) pp. 379-409.
A
preliminary version appeared in
RTA-96, LNCS 1103, 215--229.
-
Typing lambda terms in elementary logic with linear constraints,
with
P. Coppola.
Conference on Typed
Lambda-Calculus and Applications, TLCA01, LNCS 2044, 76--90, 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. 185-237.
A
preliminary version appeared in
Typed Lambda-Calculus and Applications, TLCA97, Springer, Berlin, LNCS 1210,
181--195.
-
Modal logic, linear logic, optimal lambda-reduction,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. 735-753, 1998.
Postscript version is
here.
-
Experiments in linear natural deduction, with
Andrea Masini. In Theoretical
Computer Science. vol. 176 (1997), 159--173.
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:96-97, 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, 213--241.
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):693--696, 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 197--210, 1995.
Postscript version is
here.
-
A modal view of linear logic, with
Andrea Masini.
The Journal of Symbolic Logic, vol 59(1994) no. 3, 888--899.
Postscript version is
here.
-
Proof-functional connectives and realizability, with
Franco Barbanera.
Archive for Mathematical Logic, vol. 33(1994), 189--211.
Postscript version is
here.
-
E. Boerger, G. Jaeger, H. Kleine-Buening, S. Martini, M.M. Richter,
Computer Science Logic, Selected papers of CSL'92,
LNCS 702, (Springer-Verlag, 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), 4--56;
preliminary version in International Conference on
Theoretical Aspects of Computer Software,
LNCS 526, 750--770. Postcript version is
here.
|