48 citations · 112 across the 8 of their papers we have counts for
10 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…
The Benefit of Being Non-Lazy in Probabilistic λ-calculus
Gianluca Curzi, Michele Pagani
We consider the probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specif…
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…
Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems
Michele Pagani, Sandra Alves
This volume contains a final and revised selection of papers presented at Twelfth Workshop on Developments in Computational Models (DCM 2018) and the Ninth Workshop on Intersection…
Revisiting Call-by-value Böhm trees in light of their Taylor expansion
Emma Kerinec, Giulio Manzonetto, Michele Pagani
The call-by-value lambda calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get st…
Measurable Cones and Stable, Measurable Functions
Thomas Ehrhard, Michele Pagani, Christine Tasson
We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives…
Strong Normalizability as a Finiteness Structure via the Taylor Expansion of λ-terms
Michele Pagani, Christine Tasson, Lionel Vaux
In the folklore of linear logic, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cu…
Full abstraction for probabilistic PCF
Thomas Ehrhard, Michele Pagani, Christine Tasson
We present a probabilistic version of PCF, a well-known simply typed universal functional language. The type hierarchy is based on a single ground type of natural numbers. Even if…
Call-by-value non-determinism in a linear logic type discipline
Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani
We consider the call-by-value lambda-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the re…
Applying quantitative semantics to higher-order quantum computing
Michele Pagani, Peter Selinger, Benoît Valiron
Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this pro…