48 citations · 118 across the 8 of their papers we have counts for
8 papers
Automatic Differentiation in PCF
Damiano Mazza, Michele Pagani
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…
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Alois Brunel, Damiano Mazza, Michele Pagani
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computatio…
A Strong Distillery
Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
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…
Distilling Abstract Machines (Long Version)
Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
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…
Computational Complexity of Interactive Behaviors
Ugo Dal Lago, Tobias Heindel, Damiano Mazza +1
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 bro…
An Abstract Approach to Stratification in Linear Logic
Pierre Boudes, Damiano Mazza, Lorenzo Tortora de Falco
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 abstr…
Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators
Damiano Mazza
The symmetric interaction combinators are an equally expressive variant of Lafont's interaction combinators. They are a graph-rewriting model of deterministic computation. We defin…
Linear Logic by Levels and Bounded Time Complexity
Patrick Baillot, Damiano Mazza
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,…