24 citations · 38 across the 4 of their papers we have counts for
4 papers · 1 filter
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…
Indexed realizability for bounded-time programming with references and type fixpoints
Aloïs Brunel, Antoine Madet
The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging t…
Quantitative classical realizability
Aloïs Brunel
Introduced by Dal Lago and Hofmann, quantitative realizability is a technique used to define models for logics based on Multiplicative Linear Logic. A particularity is that functio…
Church => Scott = Ptime: an application of resource sensitive realizability
Aloïs Brunel, Kazushige Terui
We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed b…