Church => Scott = Ptime: an application of resource sensitive realizability - Aloïs Brunel; Kazushige Terui (DICE, 2010)

Orthogonality and Boolean Algebras for Deduction Modulo. - Aloïs Brunel; Olivier Hermant; Clément Houtmann (TLCA, 2011)

Non-constructive complex analysis in Coq. - Aloïs Brunel (TYPES, 2011)

Indexed Realizability for Bounded-Time Programming with References and Type Fixpoints. - Aloïs Brunel; Antoine Madet (APLAS, 2012)

A Core Quantitative Coeffect Calculus. - Aloïs Brunel; Marco Gaboardi; Damiano Mazza; Steve Zdancewic (ESOP, 2014)

The monitoring power of forcing program transformations. (Transformations de forcing et algèbres de monitoring) - Aloïs Brunel (2014)

Quantitative classical realizability. - Aloïs Brunel (Inf. Comput., 2015)

Realizability models for a linear dependent PCF. - Aloïs Brunel; Marco Gaboardi (Theor. Comput. Sci., 2015)

Backpropagation in the simply typed lambda-calculus with linear negation. - Aloïs Brunel; Damiano Mazza; Michele Pagani (Proc. ACM Program. Lang., 2020)