Selected publications

Books

Maurizio Gabbrielli, Simone Martini Linguaggi di programmazione: principi e paradigmi. Seconda edizione. McGraw-Hill Italia, 2011. ISBN 88-386-6573-8. Errori di stampa noti nella seconda edizione Errori di stampa noti nella prima edizione English version: Programming Languages: Principles and Paradigms. Springer, April 2010. ISBN 978-1-84882-913-8. Series Undergraduate Topics in Computer Science, UTiCS.

Selected published papers

• Programmare per imparare la crittografia al Liceo Matematico, with M. Lodi and M. Sbaraglia. Rendiconti Sem. Mat. Univ. Pol. Torino Vol. 80(2), pages --. October 2022.
• Cryptography in Grade 10: Core Ideas with Snap! and Unplugged, with M. Lodi and M. Sbaraglia. ITiCSE '22: Proceedings of the 27th ACM Conference on on Innovation and Technology in Computer Science Education Vol. 1, pages 456-462. Dublin, July 2022.
• A Necessity-Driven Ride on the Abstraction Rollercoaster of CS1 Programming, with M. Sbaraglia, and M. Lodi. Informatics in Education, 2021, Vol. 20, No. 4, 641-682.
• The Online Course Was Great: I Would Attend It Face-to-Face, with M. Lodi, M. Sbaraglia, and S.P. Zingaro. ACM International Conference on Information Technology for Social Good (GoodIT 2021); Roma, Italy, 9-11 September 2021. ACM, New York, NY, USA.
• The Good, The Bad, and The Ugly of a Synchronous Online CS1, with M. Lodi, M. Sbaraglia, and S.P. Zingaro. ITiCSE '21: Proceedings of the 26th ACM Conference on Innovation and Technology in Computer Science Education V. 2 June 2021 Pages 660 (poster). Editorial pdf.
• Computational thinking, between Papert and Wing, with M. Lodi, in Science & Education, Springer (2021).
  A (very) preliminary (but much shorter) version, under the title Computational Thinking, between Scylla and Charybdis (2019).
• From 2-sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics, with A. Masini and M. Zorzi, ACM Transactions on Computational Logic (TOCL), vol 22(3), article 19:1-29, 2021. Also on arXiv, CoRR, April 2021.
  
• Quantum Turing Machines: computations and measurements, with S. Guerrini, and A. Masini, Applied Sciences vol. 10(16), 5551 (2020).
• The standard model for programming languages: The birth of a mathematical theory of computation, in Recent Developments in the Design and Implementation of Programming Languages, Frank S. de Boer and Jacopo Mauro (Eds), OpenAccess Series in Informatics (OASIcs), vol. 86, 8:1-8:13, November 2020.
• (Non) parliamo di pensiero computazionale, with M. Lodi, M. Sbaraglia, and S.P. Zingaro, in Didattica della Matematica, disciplina scientifica per una scuola efficace, a cura di B. D'Amore e S. Sbaragli, pp 77-78, Pitagora editrice, 2020.
• Informatica senza e con computer nella Scuola Primaria, with M. Lodi, R. Davoli, and R. Montanari, in Coding e oltre: l'informatica nella scuola, a cura di E. Nardelli, Lisciani Scuola, Teramo, (Collana: Guide per lo sviluppo professionale degli insegnanti), 2020.
• Problem Solving Olympics: an inclusive education model for learning Informatics, with R. Borchia, A. Carbonaro, G. Casadei, L. Forlizzi, and M. Lodi, Informatics in Schools: Situation, Evolution and Perspectives, ISSEP 2018, LNCS LNCS 11169, 319--335, 2018.
• Abbiamo davvero bisogno del pensiero computazionale?, with M. Lodi and E. Nardelli, Mondo Digitale, n. 72, Dicembre 2017, 1--15.
• Pensiero computazionale: una quarta competenza dopo scrivere, leggere e far di conto, il Nodo, vol. 47 (2017) 18--28 (Falco Editore, Cosenza, I).
• Programs as inscriptions, unpublished notes, August 2016. See also the talk Ipsa forma est substantia: Language(s) at the core of computer science. HaPoC Symposium at IACAP-14, 3 luglio 2014. Thessaloniki, Greece.
• Light Logics and Higher-Order Processes, with U. Dal Lago and D. Sangiorgi, Mathematical Structures in Computer Science, vol. 26(6) (2016) 969--992 (Cambridge University Press, Cambridge, UK). A shorter version appeared on Expressiveness in Concurrency, EXPRESS 2010, EPTCS, 41, 2010, pp. 46-60.
• Types in Programming Languages, between Modelling, Abstraction, and Correctness, CiE 2016: Pursuit of the Universal, LNCS 9709, 164--169, 2016.
• Several types of types in programming languages, History and Philosophy of Computing, HAPOC 2015, IFIP Advances in Information and Communication Technology 487, 216-227, Springer 2016.
• On Constructor Rewrite Systems and the Lambda-Calculus, with U. Dal Lago. Logical Methods in Computer Science, Vol. 8(3:12), 2012, pp. 1-27. 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.
• Lingua Universalis. Annali della Pubblica Istruzione, n. 4-5, 2011, pp. 65-70.
• 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, 47--62, May 2010.
• Derivational Complexity is an Invariant Cost Model with U. Dal Lago. FOPARA 2009, Springer LNCS 6324, 88--101, 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.), 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 ve rsion), 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 Andr ea Masini, in Proof Theory of Modal Logic 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 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.
• Bounded quantifiers have interval models, LFP'88: Proceedings of the 1988 ACM conference on LISP and functional programming, 164-173, 1988. doi:10.1145/62678.62699.