Selected publications

Books

Maurizio Gabbrielli, Simone Martini Linguaggi di programmazione: principi e paradigmi. McGraw-Hill Italia, 2006. ISBN 88-386-6261-4. Errori di stampa noti English version forthcoming for Springer UK. Series Undergraduate Topics in Computer Science, UTiCS.

Published papers

• 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.