Towards Constructive Homological Algebra in Type Theory. - Thierry Coquand; Arnaud Spiwack (Calculemus/MKM, 2007)

A proof of strong normalisation using domain theory. - Thierry Coquand; Arnaud Spiwack (Log. Methods Comput. Sci., 2007)

Catch Me If You Can - Looking for Type-Safe, Hierarchical, Lightweight, Polymorphic and Efficient Error Management in OCaml. - David Teller; Arnaud Spiwack; Till Varoquaux (IFL, 2008)

Extending FeatherTrait Java with Interfaces. - Luigi Liquori; Arnaud Spiwack (Theor. Comput. Sci., 2008)

FeatherTrait: A modest extension of Featherweight Java. - Luigi Liquori; Arnaud Spiwack (ACM Trans. Program. Lang. Syst., 2008)

Extending Coq with Imperative Features and Its Application to SAT Verification. - Michaël Armand; Benjamin Grégoire; Arnaud Spiwack; Laurent Théry (ITP, 2010)

Verified Computing in Homological Algebra. (Calculs vérifiés en algèbre homologique). - Arnaud Spiwack (2011)

The Rooster and the Syntactic Bracket. - Hugo Herbelin; Arnaud Spiwack (TYPES, 2013)

Abstract interpretation as anti-refinement. - Arnaud Spiwack (CoRR, 2013)

Balancing Lists: A Proof Pearl. - Guyslain Naves; Arnaud Spiwack (ITP, 2014)

Notes on axiomatising Hurkens's Paradox. - Arnaud Spiwack (CoRR, 2015)

The tree machine. - Arnaud Spiwack (CoRR, 2015)

Circuits via topoi. - Arnaud Spiwack (CoRR, 2018)

Linear Haskell: practical linearity in a higher-order polymorphic language. - Jean-Philippe Bernardy; Mathieu Boespflug; Ryan R. Newton; Simon Peyton Jones; Arnaud Spiwack (Proc. ACM Program. Lang., 2018)

Union and intersection contracts are hard, actually. - Teodoro Freund; Yann Hamdaoui; Arnaud Spiwack (DLS, 2021)

Evaluating linear functions to symmetric monoidal categories. - Jean-Philippe Bernardy; Arnaud Spiwack (Haskell, 2021)

Linear Constraints. - Jean-Philippe Bernardy; Richard A. Eisenberg; Csongor Kiss; Arnaud Spiwack; Nicolas Wu (CoRR, 2021)

Linearly qualified types: generic inference for capabilities and uniqueness. - Arnaud Spiwack; Csongor Kiss; Jean-Philippe Bernardy; Nicolas Wu; Richard A. Eisenberg (Proc. ACM Program. Lang., 2022)

Destination Calculus: A Linear 𝜆-Calculus for Purely Functional Memory Writes. - Thomas Bagrel; Arnaud Spiwack (Proc. ACM Program. Lang., 2025)