
Selected publications
Books
Selected published papers
Preliminary versions are available through this page. Please refer to the printed publication
for the final version.
 Teaching Programming in the Age of Generative AI. Keynote for ITiCSE '24: Proceedings of the 29th ACM Conference on Innovation and Technology in Computer Science Education Vol. 1, pages 12. Milan, July 2022.
 Big Ideas of Cryptography in Primary School, with M. Lodi and M.C. Carrisi. ITiCSE '24: Proceedings of the 29th ACM Conference on Innovation and Technology in Computer Science Education Vol. 1, pages 12. Milan, July 2022.
 A Natural Deduction Calculus for S4.2, with A. Masini
and M. Zorzi. Notre Dame J. Formal Logic 65 (2) 127  150, May 2024.
 The early years of Italian Theoretical Computer Science, in Pisa, in Chemins croisés entre les mathématiques, la biologie et l'epistémologie, M. Montévil, B. Bravi, J.A. PerezEscobar, A. Angelini (Eds.), Éditions SpartacusIdh (to appear, 2024).
 An Unplugged Didactical Situation on Cryptography between Informatics and Mathematics, with E.I. Bartzia, M. Lodi, M. Sbaraglia, S. Modeste, and V. DurandGuerrier.
Informatics in Education, Vol. 23(1), 25  56, 2024.
 Cryptography as a field to foster interactions between mathematics and informatics, and algorithms. Analysis of a didactical situation, with E.I. Bartzia, M. Lodi, M. Sbaraglia, S. Modeste, and V. DurandGuerrier.
13th Congress of the European Society for Research in Mathematics Education (CERME13), P. Drijverset al. (Eds.), pp. 30013008, Alfréd Rényi Institute of Mathematics and ERME, 2023.
 Cut elimination for extended sequent calculi, with A. Masini
and M. Zorzi. Bulletin of the Section of Logic, 2023, 52, 459  495.
 Programmare per imparare la crittografia al Liceo Matematico, with M. Lodi and M. Sbaraglia. Rendiconti Sem. Mat. Univ. Pol. Torino Vol. 80, 2(2022), 4981. July 2023.
 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 Innovation and Technology in Computer Science Education Vol. 1, pages 456462. Dublin, July 2022.
 A NecessityDriven Ride on the Abstraction Rollercoaster of CS1 Programming, with M. Sbaraglia, and M. Lodi. Informatics in Education, 2021, Vol. 20, No. 4, 641682.
 The Online Course Was Great: I Would Attend It FacetoFace, with M. Lodi, M. Sbaraglia, and S.P. Zingaro. ACM International Conference on Information Technology for Social Good (GoodIT 2021); Roma, Italy, 911 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 2sequents 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:129, 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:18: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 7778, 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, 319335, 2018.
 Abbiamo davvero bisogno del pensiero computazionale?, with M. Lodi and E. Nardelli, Mondo Digitale, n. 72, Dicembre 2017, 115.
 Pensiero computazionale: una quarta competenza dopo scrivere, leggere e far di conto, il Nodo, vol. 47 (2017) 1828 (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 IACAP14, 3 luglio 2014.
Thessaloniki, Greece.
 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 ve
rsion), 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 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.

Bounded quantifiers have interval models, LFP'88: Proceedings of the 1988 ACM conference on LISP and functional programming,
164173, 1988. doi:10.1145/62678.62699.
