In February 2012, I signed the Cost of Knowledge boycott against Elsevier. As a consequence, from then onward I do not referee or do any editorial work for Elsevier, nor submit papers to its journals, unless this causes inconveniences to my coauthors. Examples of wellknown Elsevier journals in my research field are Theoretical Computer Science, Information and Computation and the Annals of Pure and Applied Logic.
Personally, I believe that, in a nottoodistant future, traditional journal publishing will be supplanted by more modern systems, such as online interactive publications. If you care to know more about my position on this, you may read this text.
with Ugo Dal Lago, Marc de Visme and Akira Yoshimizu, Intersection Types and Runtime Errors in the PiCalculus. In Proceedings of the ACM on Programming Languages, 3(POPL:7), 2019.
We introduce a type system for the πcalculus which is designed to guarantee that typable processes are wellbehaved, namely they never produce a runtime error and, even if they may diverge, there is always a chance for them to "finish their work", i.e., to reduce to an idle process. The introduced type system is based on nonidempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is Π^0_2complete, there is a way to show that the system is complete, i.e., that any wellbehaved process is typable, although for obvious reasons infinitely many derivations need to be considered. @Article{DalLagodeVismeMazzaYoshimizu, 
with Luc Pellissier and Pierre Vial, Polyadic Approximations, Fibrations and Intersection Types. In Proceedings of the ACM on Programming Languages, 2(POPL:6), 2018.
Starting from an exact correspondence between linear approximations and nonidempotent intersection types, we develop a general framework for building systems of intersection types characterizing normalization properties. We show how this construction, which uses in a fundamental way Melliès and Zeilberger's ``type systems as functors'' viewpoint, allows us to recover equivalent versions of every well known intersection type system (including Coppo and Dezani's original system, as well as its nonidempotent variants independently introduced by Gardner and de Carvalho). We also show how new systems of intersection types may be built almost automatically in this way. @Article{MazzaPellissierVial, 
Infinitary Affine Proofs. Mathematical Structures in Computer Science, 27(5):581602, 2017. Submitted in 2012 and accepted in 2014.
Even though the multiplicativeadditive fragment of linear logic forbids structural rules in general, is does admit a bounded form of exponential modalities enjoying a bounded form of structural rules. The approximation theorem, originally proved by Girard, states that if full linear logic proves a propositional formula, then the multiplicativeadditive fragment proves every bounded approximation of it. This may be understood as the fact that multiplicativeadditive linear logic is somehow dense in full linear logic. Our goal is to give a technical formulation of this informal remark. We introduce a Cauchycomplete space of infinitary affine termproofs and we show that it yields a fully complete model of multiplicative exponential polarized linear logic, in the style of Girard's ludics. Moreover, the subspace of finite termproofs, which is a model of multiplicative polarized linear logic, is dense in the space of all termproofs. @Article{Mazza:InfAffProofsMSCS, 
with Pierre Boudes and Lorenzo Tortora de Falco, An Abstract Approach to Stratification in Linear Logic. Information and Computation, 241:3261, 2015. Submitted in 2011 and accepted in 2013.
We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cutelimination procedure (the socalled light logics), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a general categorical construction applicable to all models of linear logic. We thus learn that stratification may be formulated independently of exponential modalities; when it is forced to be connected to exponential modalities, it yields interesting complexity properties. In particular, from our analysis stem three alternative reformulations of Baillot and Mazza's linear logic by levels: one geometric, one interactive, and one semantic. @Article{BoudesMazzaTortora:L3SemIC, 
The True Concurrency of Differential Interaction Nets. Mathematical Structures in Computer Science, 28(7):10971125, 2018. Submitted in 2010 and accepted in 2013.
We analyze the reduction of differential interaction nets from the point of view of socalled ``true concurrency'', that is, employing a noninterleaving model of parallelism. More precisely, we associate with each differential interaction net an event structure describing its reduction. We show how differential interaction nets are only able to generate confusionfree event structures, and we argue that this is a serious limitation in terms of the concurrent behaviors they may express. In fact, confusion is an extremely elementary phenomenon in concurrency (for example, it already appears in CCS with just prefixing and parallel composition) and we show how its presence is preserved by any encoding respecting the degree of distribution and the reduction semantics. We thus infer that no reasonably expressive process calculus may be satisfactorily encoded in differential interaction nets. We conclude with an analysis of one such encoding proposed by Ehrhard and Laurent, and argue that it does not contradict our claims, but rather supports them. @Article{Mazza:TrueConcMSCS, 
with Patrick Baillot, Linear Logic by Levels and Bounded Time Complexity. Theoretical Computer Science, 411(2):470503, 2010.
We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofsasprograms correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indexes, which allows us to extend Girard's systems while keeping the same complexity properties. In particular, it turns out that Girard's systems may be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for developing lambdacalculus type assignment systems with more efficient typing algorithms than existing ones. @Article{BaillotMazza:L3TCS, 
Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators. Logical Methods in Computer Science, 5(4:6), 2009.
The symmetric interaction combinators are an equally expressive variant of Lafont's interaction combinators. They are a graphrewriting model of deterministic computation. We define two notions of observational equivalence for them, analogous to normal form and head normal form equivalence in the lambdacalculus. Then, we prove a full abstraction result for each of the two equivalences. This is obtained by interpreting nets as certain subsets of the Cantor space, called edifices, which play the same role as Boehm trees in the theory of the lambdacalculus. @Article{Mazza:EdificesLMCS, 
A Denotational Semantics for the Symmetric Interaction Combinators. Mathematical Structures in Computer Science, 17(3):527562, 2007.
The symmetric interaction combinators are a variant of Lafont's interaction combinators. They enjoy a weaker universality property with respect to interaction nets, but are equally expressive. They are a model of deterministic distributed computation, sharing the good properties of Turing machines (elementary reductions) and of the λcalculus (higherorder functions, parallel execution). We introduce a denotational semantics for this system, inspired by the relational semantics for linear logic, proving an injectivity and full completeness result for it. We also consider the algebraic semantics defined by Lafont, and prove that the two are strongly related. @Article{Mazza:CombSemMSCS, 
Observational Equivalence for the Interaction Combinators and Internal Separation. Electronic Notes in Theoretical Computer Science, 176(1):113137, 2007.
We define an observational equivalence for Lafont's interaction combinators, which we prove to be the least discriminating nontrivial congruence on total nets (nets admitting a deadlockfree normal form) respecting reduction. More interestingly, this equivalence enjoys an internal separation property similar to that of Böhm's Theorem for the λcalculus. @Article{Mazza:CombSepENTCS, 
Linear Logic and Polynomial Time. Mathematical Structures in Computer Science, 16(6):947988, 2006.
Light and Elementary Linear Logic, the cornerstones at the interface between logic and implicit computational complexity, were originally introduced by Girard as "standalone" logical systems with a (somewhat awkward) sequent calculus of their own. The latter has later been reformulated by Danos and Joinet as a proper subsystem of linear logic, whose proofs satisfy a certain structural condition. We extend this approach to polytime computation, finding two solutions: the first one, obtained by a simple extension of Danos and Joinet's condition, closely resembles Asperti's Light Affine Logic and enjoys polystep strong normalization (the polynomial bound does not depend on the reduction strategy); the second one, which needs more complex conditions, exactly corresponds to Girard's Light Linear Logic. @Article{Mazza:LLandPTimeMSCS, 
NonLinearity as the Metric Completion of Linearity. In Proceedings of TLCA, LNCS 7941, pp. 314, 2013. Errata corrige.
We summarize some recent results showing how the lambdacalculus may be obtained by considering the metric completion (with respect to a suitable notion of distance) of a space of affine lambdaterms, i.e., lambdaterms in which abstractions bind variables appearing at most once. This formalizes the intuitive idea that multiplicative additive linear logic is ``dense'' in full linear logic (in fact, a prooftheoretic version of the abovementioned construction is also possible). We argue that thinking of nonlinearity as the ``limit'' of linearity gives an interesting point of view on wellknown properties of the lambdacalculus and its relationship to computational complexity (through lambdacalculi whose normalization is timebounded). @InProceedings{Mazza:LambdaMetricsTLCA, 
Church Meets Cook and Levin. In Proceedings of LICS, ACM, pp. 827836, 2016.
The CookLevin theorem (the statement that SAT is NPcomplete) is a central result in structural complexity theory. Is it possible to prove it using the lambdacalculus instead of Turing machines? We address this question via the notion of affine approximation, which offers the possibility of using ordertheoretic arguments, in contrast to the machinelevel arguments employed in standard proofs. However, due to the size explosion problem in the lambdacalculus (a linear number of reduction steps may generate exponentially big terms), a naive transliteration of the proof of the CookLevin theorem fails. We propose to fix this mismatch using the author's recently introduced parsimonious lambdacalculus, reproving the CookLevin theorem and several related results in this higherorder framework. We also present an interesting relationship between approximations and intersection types, and discuss potential applications. @InProceedings{Mazza:LICS2016, 
with Beniamino Accattoli and Pablo Barenbaum, A Strong Distillery. In Proceedings of APLAS, LNCS 9458, pp. 120, 2015.
Abstract machines for the strong evaluation of lambdaterms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higherorder logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmostoutermost (callbyname) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard microstep strategy for explicit substitutions, namely linear leftmostoutermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments. @InProceedings{AccattoliBarenbaumMazza:APLAS2015, 
with Luc Pellissier, A Functorial Bridge between the Infinitary Affine LambdaCalculus and Linear Logic. In Proceedings of ICTAC, LNCS 9399, pp. 140161, 2015.
It is a well known intuition that the exponential modality of linear logic may be seen as a form of limit. Recently, Melliès, Tabareau and Tasson gave a categorical account for this intuition, whereas the first author provided a topological account, based on an infinitary syntax. We relate these two different views by giving a categorical version of the topological construction, yielding two benefits: on the one hand, we obtain canonical models of the infinitary affine lambdacalculus introduced by the first author; on the other hand, we find an alternative formula for computing free commutative comonoids in models of linear logic with respect to the one presented by Melliès et al. @InProceedings{MazzaPellissier:ICTAC2015, 
Simple Parsimonious Types and Logarithmic Space. In Proceedings of CSL, LIPIcs 41, pp. 2440, 2015.
We present a functional characterization of deterministic logspacecomputable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simplytyped and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higherorder languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode firstorder logic with deterministic closure), whereas soundness is established by executing terms on a token machine (using the geometry of interaction). @InProceedings{Mazza:CSL2015, 
with Kazushige Terui, Parsimonious Types and Nonuniform Computation. In Proceedings of ICALP, Part II, LNCS 9135, pp. 350361, 2015.
We consider a nonuniform affine lambdacalculus, called parsimonious, and endow its terms with two type disciplines: simplytyped and with linear polymorphism. We show that the terms of string type into Boolean type characterize the class L/poly in the first case, and P/poly in the second. Moreover, we relate this characterization to that given by the second author in terms of Boolean proof nets, highlighting continuous affine approximations as the bridge between the two approaches to nonuniform computation. @InProceedings{MazzaTerui:ICALP2015, 
with Beniamino Accattoli and Pablo Barenbaum, Distilling Abstract Machines. In Proceedings of ICFP, ACM, pp. 363376, 2014.
It is wellknown that many environmentbased abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between bigstep calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environmentbased abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in callbyname, callbyvalue, and callbyneed, catching many machines in the literature. We start by distilling the KAM, the CEK, and the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. the LSC is a complexitypreserving abstraction of abstract machines. @InProceedings{AccattoliBarenbaumMazza:ICFP2014, 
NonUniform Polytime Computation in the Infinitary Affine LambdaCalculus. In Proceedings of ICALP, Part II, LNCS 8573, pp. 305317, 2014.
We give an implicit, functional characterization of the class of nonuniform polynomial time languages, based on an infinitary affine lambdacalculus and on previously defined boundedcomplexity subsystems of linear (or affine) logic. The fact that the characterization is implicit means that the complexity is guaranteed by structural properties of programs rather than explicit resource bounds. As a corollary, we obtain a proof of the (already known) Pcompleteness of the normalization problem for the affine lambdacalculus which mimics in an interesting way the proof of the CookLevin theorem. This suggests that the relationship between affine and usual lambdacalculus is deeply similar to that between Boolean circuits and Turing machines. @InProceedings{Mazza:ICALP2014, 
with Aloïs Brunel, Marco Gaboardi and Steve Zdancewic, A Core Quantitative Coeffect Calculus. In Proceedings of ESOP, LNCS 8410, pp. 351370, 2014.
Linear logic is well known for its resourceawareness, which has inspired the design of several resource management mechanisms in programming language design. The resourceawareness of linear logic is essentially due to the distinction between linear, singleuse data and nonlinear, reusable data. This latter is marked by the socalled exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad. Monadic notions of computation are wellestablished mechanisms used to express effects in pure functional languages. Less wellestablished is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language, called lRPCF, inspired by a generalized interpretation of the exponential modality. In lRPCF the exponential modality carries a labelan element of a semiringthat provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis. @InProceedings{BrunelGaboardiMazzaZdancewic:BoundedExp, 
with Andrei Dorman, A Hierarchy of Expressiveness in Concurrent Interaction Nets. In Proceedings of CONCUR, LNCS 8052, pp. 197211, 2013.
We give separation results, in terms of expressiveness, concerning all the concurrent extensions of interaction nets defined so far in the literature: we prove that multirule interaction nets (of which Ehrhard and Regnier's differential interaction nets are a special case) are strictly less expressive than multiwire interaction nets (which include Beffara and Maurel's concurrent nets and Honda and Laurent's version of polarized proof nets); these, in turn, are strictly less expressive than multiport interaction nets (independently introduced by Alexiev and the second author), although in a milder way. These results are achieved by providing a notion of barbed bisimilarity for interaction nets which is general enough to adapt to all systems but is still concrete enough to allow (hopefully) convincing separation results. This is itself a contribution of the paper. @InProceedings{DormanMazza:INHierarchyCONCUR, 
An Infinitary Affine LambdaCalculus Isomorphic to the Full LambdaCalculus. In Proceedings of LICS, IEEE Computer Society, pp. 471480, 2012. Errata corrige.
It is well known that the real numbers arise from the metric completion of the rational numbers, with the metric induced by the usual absolute value. We seek a computational version of this phenomenon, with the idea that the role of the rationals should be played by the affine lambdacalculus, whose dynamics is finitary; the full lambdacalculus should then appear as a suitable metric completion of the affine lambdacalculus. This paper proposes a technical realization of this idea: an affine lambdacalculus is introduced, based on a fragment of intuitionistic multiplicative linear logic; the calculus is endowed with a notion of distance making the set of terms an incomplete metric space; the completion of this space is shown to yield an infinitary affine lambdacalculus, whose quotient under a suitable partial equivalence relation is exactly the full (nonaffine) lambdacalculus. We also show how this construction brings interesting insights on some standard rewriting properties of the lambdacalculus (finite developments, confluence, standardization, head normalization and solvability). @InProceedings{Mazza:LICS2012, 
with Neil J. Ross, Full Abstraction for SetBased Models of the Symmetric Interaction Combinators. In Proceedings of FOSSACS, LNCS 7213, pp. 316330, 2012.
The symmetric interaction combinators are a model of distributed and deterministic computation based on Lafont's interaction nets, a special form of graph rewriting. The interest of the symmetric interaction combinators lies in their universality, that is, the fact that they may encode all other interaction net systems; for instance, several implementations of the lambdacalculus in the symmetric interaction combinators exist, related to Lamping's sharing graphs for optimal reduction. A certain number of observational equivalences were introduced for this system, by Lafont, Fernandez and Mackie, and the first author. In this paper, we study the problem of full abstraction with respect to one of these equivalences, using a class of very simple denotational models based on pointed sets. @InProceedings{MazzaRoss:FOSSACS2012, 
with Michele Pagani, The Separation Theorem for Differential Interaction Nets. In Proceedings of LPAR, LNAI 4790, pp. 393407, 2007.
Differential interaction nets (DIN) have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proofnets. We prove that DIN enjoy an internal separation property: given two different normal nets, there exists a dual net separating them, in analogy with Böhm's theorem for the λcalculus. Our result implies in particular the faithfulness of every nontrivial denotational model of DIN (such as Ehrhard's finiteness spaces). We also observe that internal separation does not hold for linear logic proofnets: our work points out that this failure is due to the fundamental asymmetry of linear logic exponential modalities, which are instead completely symmetric in DIN. @InProceedings{MazzaPagani:LPAR07, 
Edifices and Full Abstraction for the Symmetric Interaction Combinators. In Proceedings of TLCA, LNCS 4583, pp. 305320, 2007. Superseded by the journal paper.
The symmetric interaction combinators are a variant of Lafont's interaction combinators. They are a graphrewriting model of parallel deterministic computation. We define a notion analogous to that of head normal form in the λcalculus, and make a semantical study of the corresponding observational equivalence. We associate with each net a compact metric space, called edifice, and prove that two nets are observationally equivalent iff they have the same edifice. Edifices may therefore be compared to Böhm trees in infinite ηnormal form, or to Nakajima trees, and give a precise topological account of phenomena like infinite ηexpansion. @InProceedings{Mazza:EdificesTLCA07, 
Multiport Interaction Nets and Concurrency. In Proceedings of CONCUR, LNCS 3653, pp. 2135, 2005.
We consider an extension of Lafont's Interaction Nets, called Multiport Interaction Nets, and show that they are a model of concurrent computation by encoding the full πcalculus in them. We thus obtain a faithful graphical representation of the πcalculus in which every reduction step is decomposed in fully local graphrewriting rules. @InProceedings{Mazza:CONCUR05, 
with Marc de Visme, On the Concurrent Meaning of Logical Correctness. Unpublished, 2017.
Following Girard, proof nets naturally suggest the introduction of more general prooflike objects, called nets (or proof structures in Girard's original terminology), which may not be logically correct but which may still have nontrivial computational behavior. For instance, Ehrhard and Laurent's encoding of the picalculus in differential interaction nets maps a host of processes to incorrect nets. It is then natural to ask which processes are mapped to proof nets or, in other words, what meaning does logical correctness have when seen through Ehrhard and Laurent's encoding. We answer this question by showing that logical correctness ensures a form of deadlockfreedom. 
On Time and Space in Higher Order Boolean Circuits. Unpublished, 2016. Abstract of the talk presented at LCC 2016.

with Ugo Dal Lago, Tobias Heindel and Daniele Varacca, Computational Complexity of Interactive Behaviors. ArXiv preprint, arXiv:1209.0663v1 [cs.CC], 2012.
The theory of computational complexity focuses on functions and, hence, studies programs whose interactive behavior is reduced to a simple question/answer pattern. We propose a broader theory whose ultimate goal is expressing and analyzing the intrinsic difficulty of fully general interactive behaviors. To this extent, we use standard tools from concurrency theory, including labelled transition systems (formalizing behaviors) and their asynchronous extension (providing causality information). Behaviors are implemented by means of a multiprocessor machine executing CCSlike processes. The resulting theory is shown to be consistent with the classical definitions: when we restrict to functional behaviors (i.e., question/answer patterns), we recover several standard computational complexity classes. @TechReport{DLHMV:BehaviorComplexity, 
Polyadic Approximations in Logic and Computation. Habilitation thesis, Université Paris 13, 2017.
@PhDThesis{Mazza:Hab, 
Interaction Nets: Semantics and Concurrent Extensions. Ph.D. thesis, Université de la Méditerranée/Università degli Studi Roma Tre, 2006. The thesis was awarded the Prix de Thèse 2006 de l'Université de la Méditerranée.
@PhDThesis{Mazza:PhDThesis, 
Pi et Lambda. Une étude sur la traduction des lambdatermes dans le picalcul. Mémoire de DEA (Master's thesis), Université de la Méditerranée (AixMarseille 2), 2003 (in french).

Logica Lineare e Complessità Computazionale. Tesi di Laurea (Master's thesis), Università degli Studi Roma Tre, 2002 (in italian).
@PhdThesis{Mazza:TesiLaurea, 