Damiano Mazza
Home page
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 well-known Elsevier journals in my research field are Theoretical Computer Science, Information and Computation and the Annals of Pure and Applied Logic.
More recently (2019), I decided to boycott in the same way any publication venue, including conferences, which does not adhere to an open access policy. This includes LICS, one of the flagship conferences of my research field.
Personally, I believe that traditional journal publishing should be supplanted by more modern systems, such as online interactive publications, and that, at the same time, TCS conferences should stop having published proceedings and regain their original role of pure dissemination venues. If you care to know more about my position on this, you may read this text.
|
with Michele Pagani, Automatic Differentiation in PCF. In Proceedings of the ACM on Programming Languages, 5(POPL:28), 2021.
We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except for a set of Lebesgue measure zero. Stated otherwise, there are inputs on which AD is incorrect, but the probability of randomly choosing one such input is zero. Our result is in fact more precise, in that the set of failure points admits a more explicit description: for example, in case the primitive functions are just constants, addition and multiplication, the set of points where AD fails is contained in a countable union of zero sets of polynomials. @Article{MazzaPagani:POPL2021, |
|
with Aloïs Brunel and Michele Pagani, Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation. In Proceedings of the ACM on Programming Languages, 4(POPL:64), 2020.
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field called differentiable programming, the aim of which is to express computational graphs more synthetically and modularly by resorting to actual programming languages endowed with control flow operators and higher-order combinators, such as map and fold. In this paper, we extend the backpropagation algorithm to a paradigmatic example of such a programming language: we define a compositional program transformation from the simply-typed lambda-calculus to itself augmented with a notion of linear negation, and prove that this computes the gradient of the source program with the same efficiency as first-order backpropagation. The transformation is completely effect-free and thus provides a purely logical understanding of the dynamics of backpropagation. @Article{BrunelMazzaPagani, |
|
with Ugo Dal Lago, Marc de Visme and Akira Yoshimizu, Intersection Types and Runtime Errors in the Pi-Calculus. 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 well-behaved, namely they never produce a run-time 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 non-idempotent 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_2-complete, there is a way to show that the system is complete, i.e., that any well-behaved 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. Erratum: Theorem 2.4 is false with the definitions given in the paper. Fortunately this has no consequence for the rest of the paper. See the Preface of my habilitation thesis for the correction.
Starting from an exact correspondence between linear approximations and non-idempotent 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 non-idempotent 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):581-602, 2017. Submitted in 2012 and accepted in 2014.
Even though the multiplicative-additive 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 multiplicative-additive fragment proves every bounded approximation of it. This may be understood as the fact that multiplicative-additive linear logic is somehow dense in full linear logic. Our goal is to give a technical formulation of this informal remark. We introduce a Cauchy-complete space of infinitary affine term-proofs 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 term-proofs, which is a model of multiplicative polarized linear logic, is dense in the space of all term-proofs. @Article{Mazza:InfAffProofsMSCS, |
|
with Pierre Boudes and Lorenzo Tortora de Falco, An Abstract Approach to Stratification in Linear Logic. Information and Computation, 241:32-61, 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 cut-elimination procedure (the so-called 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):1097-1125, 2018. Submitted in 2010 and accepted in 2013.
We analyze the reduction of differential interaction nets from the point of view of so-called ``true concurrency'', that is, employing a non-interleaving 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 confusion-free 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):470-503, 2010.
We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs 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 lambda-calculus 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 graph-rewriting model of deterministic computation. We define two notions of observational equivalence for them, analogous to normal form and head normal form equivalence in the lambda-calculus. 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 lambda-calculus. @Article{Mazza:EdificesLMCS, |
|
A Denotational Semantics for the Symmetric Interaction Combinators. Mathematical Structures in Computer Science, 17(3):527-562, 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 (higher-order 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):113-137, 2007.
We define an observational equivalence for Lafont's interaction combinators, which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free 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):947-988, 2006.
Light and Elementary Linear Logic, the cornerstones at the interface between logic and implicit computational complexity, were originally introduced by Girard as "stand-alone" 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, |
|
Non-Linearity as the Metric Completion of Linearity. In Proceedings of TLCA, LNCS 7941, pp. 3-14, 2013. Errata corrige.
We summarize some recent results showing how the lambda-calculus may be obtained by considering the metric completion (with respect to a suitable notion of distance) of a space of affine lambda-terms, i.e., lambda-terms 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 proof-theoretic version of the above-mentioned construction is also possible). We argue that thinking of non-linearity as the ``limit'' of linearity gives an interesting point of view on well-known properties of the lambda-calculus and its relationship to computational complexity (through lambda-calculi whose normalization is time-bounded). @InProceedings{Mazza:LambdaMetricsTLCA, |
|
with Aloÿs Dufour, Böhm and Taylor for All!. In Proceedings of FSCD, LIPICS, 26:1-26:20, 2024.
Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, Taylor approximations provide a quantitative account of the behavior of programs and are well-known to be connected to intersection types. The key relation between these two notions of approximations is a commutation theorem, roughly stating that Taylor approximations of Böhm trees are the same as Böhm trees of Taylor approximations. Böhm and Taylor approximations are available for several variants or extensions of the lambda-calculus and, in some cases, commutation theorems are known. In this paper, we define Böhm and Taylor approximations and prove the commutation theorem in a very general setting. We also introduce (non-idempotent) intersection types at this level of generality. From this, we show how the commutation theorem and intersection types may be applied to any calculus embedding in a sufficiently nice way into our general calculus. All known Böhm-Taylor commutation theorems, as well as new ones, follow by this uniform construction. @inproceedings{DufourMazza:FSCD2024, |
|
with Emmanuel Hainry and Romain Péchoux, Polynomial time over the reals with parsimony. In Proceedings of FLOPS, LNCS 12073, pp. 50-65, 2020.
We provide a characterization of Ko's class of polynomial time computable functions over real numbers. This characterization holds for a stream based language using a parsimonious type discipline, a variant of propositional linear logic. We obtain a first characterization of polynomial time computations over the reals on a higher-order functional language using a linear/affine type system. @inproceedings{HainryMazzaPechoux:FLOPS2020, |
|
Church Meets Cook and Levin. In Proceedings of LICS, ACM, pp. 827-836, 2016.
The Cook-Levin theorem (the statement that SAT is NP-complete) is a central result in structural complexity theory. Is it possible to prove it using the lambda-calculus instead of Turing machines? We address this question via the notion of affine approximation, which offers the possibility of using order-theoretic arguments, in contrast to the machine-level arguments employed in standard proofs. However, due to the size explosion problem in the lambda-calculus (a linear number of reduction steps may generate exponentially big terms), a naive transliteration of the proof of the Cook-Levin theorem fails. We propose to fix this mismatch using the author's recently introduced parsimonious lambda-calculus, reproving the Cook-Levin theorem and several related results in this higher-order 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. 1-20, 2015.
Abstract machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) 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 micro-step strategy for explicit substitutions, namely linear leftmost-outermost 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 Lambda-Calculus and Linear Logic. In Proceedings of ICTAC, LNCS 9399, pp. 140-161, 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 lambda-calculus 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. 24-40, 2015.
We present a functional characterization of deterministic logspace-computable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simply-typed and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higher-order languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode first-order 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 Non-uniform Computation. In Proceedings of ICALP, Part II, LNCS 9135, pp. 350-361, 2015.
We consider a non-uniform affine lambda-calculus, called parsimonious, and endow its terms with two type disciplines: simply-typed 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 non-uniform computation. @InProceedings{MazzaTerui:ICALP2015, |
|
with Beniamino Accattoli and Pablo Barenbaum, Distilling Abstract Machines. In Proceedings of ICFP, ACM, pp. 363-376, 2014.
It is well-known that many environment-based 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 big-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based 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 call-by-name, call-by-value, and call-by-need, 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 complexity-preserving abstraction of abstract machines. @InProceedings{AccattoliBarenbaumMazza:ICFP2014, |
|
Non-Uniform Polytime Computation in the Infinitary Affine Lambda-Calculus. In Proceedings of ICALP, Part II, LNCS 8573, pp. 305-317, 2014.
We give an implicit, functional characterization of the class of non-uniform polynomial time languages, based on an infinitary affine lambda-calculus and on previously defined bounded-complexity 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) P-completeness of the normalization problem for the affine lambda-calculus which mimics in an interesting way the proof of the Cook-Levin theorem. This suggests that the relationship between affine and usual lambda-calculus 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. 351-370, 2014.
Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. The resource-awareness of linear logic is essentially due to the distinction between linear, single-use data and non-linear, reusable data. This latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad. Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established 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 label--an element of a semiring--that 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. 197-211, 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 Lambda-Calculus Isomorphic to the Full Lambda-Calculus. In Proceedings of LICS, IEEE Computer Society, pp. 471-480, 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 lambda-calculus, whose dynamics is finitary; the full lambda-calculus should then appear as a suitable metric completion of the affine lambda-calculus. This paper proposes a technical realization of this idea: an affine lambda-calculus 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 lambda-calculus, whose quotient under a suitable partial equivalence relation is exactly the full (non-affine) lambda-calculus. We also show how this construction brings interesting insights on some standard rewriting properties of the lambda-calculus (finite developments, confluence, standardization, head normalization and solvability). @InProceedings{Mazza:LICS2012, |
|
with Neil J. Ross, Full Abstraction for Set-Based Models of the Symmetric Interaction Combinators. In Proceedings of FOSSACS, LNCS 7213, pp. 316-330, 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 lambda-calculus 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. 393-407, 2007.
Differential interaction nets (DIN) have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. 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 non-trivial denotational model of DIN (such as Ehrhard's finiteness spaces). We also observe that internal separation does not hold for linear logic proof-nets: 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. 305-320, 2007. Superseded by the journal paper.
The symmetric interaction combinators are a variant of Lafont's interaction combinators. They are a graph-rewriting 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. 21-35, 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 graph-rewriting rules. @InProceedings{Mazza:CONCUR05, |
|
An Axiomatic Notion of Approximation for Programming Languages and Machines. Unpublished, 2021.
|
|
Towards a Sheaf-Theoretic Definition of Decision Problems. Unpublished, 2019. Abstract of a talk presented at DICE-FOPARA 2019.
We sketch a functorial approach to decision problems, making some remarks on how one may define these to be shaves on suitable sites, and the consequences that this has. Some minor results are given (without proofs) but otherwise this is just a synthetic report about work in progress. |
|
with Marc de Visme, On the Concurrent Meaning of Logical Correctness. Unpublished, 2017.
Following Girard, proof nets naturally suggest the introduction of more general proof-like objects, called nets (or proof structures in Girard's original terminology), which may not be logically correct but which may still have non-trivial computational behavior. For instance, Ehrhard and Laurent's encoding of the pi-calculus 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 deadlock-freedom. |
|
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 CCS-like 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 lambda-termes dans le pi-calcul. Mémoire de DEA (Master's thesis), Université de la Méditerranée (Aix-Marseille 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, |