Arnaud Spiwack's publications

Version & licenses
Creative Commons License
Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard Eisenberg: Linearly Qualified Types: Generic inference for capabilities and uniqueness.
In: Proceedings of the ACM on Programming LanguagesVolume 6Issue ICFP (ICFP 2022).
(2022).
pdfarXivSources on Github
Teodoro Freund, Yann Hamdaoui, Arnaud Spiwack: Union and intersection contracts are hard, actually.
In: 17th ACM SIGPLAN International Symposium on Dynamic Languages (DLS 2021).
(2021).
pdfarXivSources on Github
Jean-Philippe Bernardy, Arnaud Spiwack: Evaluating Linear Functions to Symmetric Monoidal Categories.
In: 14th ACM SIGPLAN International Symposium on Haskell (Haskell Symposium 2021).
(2021).
pdfarXiv
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack: Linear Haskell: practical linearity in a higher-order polymorphic language.
In: 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).
(2018).
pdfarXivSources on Github
Arnaud Spiwack: Circuits via topoi.
Draft, (2015).
pdfSources on Github
Arnaud Spiwack: Notes on axiomatising Hurkens's paradox.
Note, (2015).
pdfarXivSources on Github
Arnaud Spiwack: The tree machine.
Working paper, (2015).
pdfarXivSources on Github
Arnaud Spiwack: A dissection of L.
Submitted, (2014).
pdf
Guyslain Naves, Arnaud Spiwack: Balancing lists: a proof pearl.
In: Interactive Theorem Proving.
(2014).
pdfarXivSources on Github
Arnaud Spiwack: Abstract interpretation as anti-refinement.
Working paper, (2013).
pdfarXiv
Hugo Herbelin, Arnaud Spiwack: The Rooster and the Syntactic Bracket.
In: 19th International Conference on Types for Proofs and Programs.
(2013).
pdfarXiv
Arnaud Spiwack: Verified Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory.
PhD. thesis, École Polytechnique, Palaiseau, France, (2011).
pdfpresentationHAL: Hyper Articles en Ligne.webpage
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry: Extending Coq with Imperative Features and its Application to SAT Verification.
In: Interactive Theorem Proving.
(2010).
pdf
Thierry Coquand, Arnaud Spiwack: Constructively Finite?
In: Contribuciones científicas en honor de Mirian Andrés Gómez.
Publicaciones de la Universidad de La Rioja, (2010).
pdf
Arnaud Spiwack: An abstract type for constructing tactics in Coq.
In: Proof Search in Type Theory.
(2010).
pdf
Arnaud Spiwack, David Teller, Till Varoquaux: Catch me if you can: Looking for type-safe, hierarchical, lightweight, polymorphic and efficient error management in OCaml.
In: Implementation and Application of Functional Languages.
(2008).
pdf
Luigi Liquori, Arnaud Spiwack: Extending FeatherTrait Java with Interfaces.
Theoretical Computer Science.
(2008).
pdf
Luigi Liquori, Arnaud Spiwack: FeatherTrait: A Modest Extension of Featherweight Java.
ACM Transactions on Programming Languages and Systems.
(2008).
pdf
Thierry Coquand, Arnaud Spiwack: Towards Constructive Homological Algebra in Type Theory.
In: CALCULEMUS.
(2007).
pdf
Thierry Coquand, Arnaud Spiwack: A Proof of Strong Normalisation Using Domain Theory.
Logical Methods in Computer Science.
(2007).
pdfarXiv
Thierry Coquand, Arnaud Spiwack: A Proof of Strong Normalisation using Domain Theory.
In: Logic In Computer Science.
(2006).
pdf