Linear Haskell: practical linearity in a higher-order polymorphic language JP Bernardy, M Boespflug, RR Newton, S Peyton Jones, A Spiwack Proceedings of the ACM on Programming Languages 2 (POPL), 1-29, 2017 | 143 | 2017 |
Extending Coq with Imperative Features and Its Application to SAT Verification M Armand, B Grégoire, A Spiwack, L Théry International Conference on Interactive Theorem Proving, 83-98, 2010 | 94 | 2010 |
FeatherTrait: A modest extension of Featherweight Java L Liquori, A Spiwack ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (2), 11, 2008 | 71 | 2008 |
A proof of strong normalisation using domain theory T Coquand, A Spiwack Logical methods in computer science 3, 2007 | 45 | 2007 |
Towards constructive homological algebra in type theory T Coquand, A Spiwack International Conference on Mathematical Knowledge Management, 40-54, 2007 | 28 | 2007 |
Constructively Finite? T Coquand, A Spiwack Universidad de La Rioja, 2010 | 24* | 2010 |
Extending feathertrait java with interfaces L Liquori, A Spiwack Theoretical Computer Science 398 (1-3), 243-260, 2008 | 16 | 2008 |
Verified Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory A Spiwack | 10 | 2011 |
The rooster and the syntactic bracket H Herbelin, A Spiwack 19th International Conference on Types for Proofs and Programs (TYPES 2013 …, 2014 | 8 | 2014 |
Ajouter des entiers machine à Coq A Spiwack | 8 | 2006 |
An abstract type for constructing tactics in Coq A Spiwack Proof Search in Type Theory, 2010 | 7 | 2010 |
Linearly qualified types: generic inference for capabilities and uniqueness A Spiwack, C Kiss, JP Bernardy, N Wu, RA Eisenberg Proceedings of the ACM on Programming Languages 6 (ICFP), 137-164, 2022 | 6 | 2022 |
A dissection of L A Spiwack Unpublished draft, 2014 | 6 | 2014 |
Featherweight-trait Java: a trait-based extension for FJ L Liquori, A Spiwack INRIA Sophia Antipolis-Méditerranée; INRIA, 2004 | 6 | 2004 |
Coq 8.4 reference manual P Boutillier, S Glondu, B Grégoire, H Herbelin, P Letouzey, PM Pédrot, ... Inria, 2014 | 5 | 2014 |
Abstract interpretation as anti-refinement A Spiwack arXiv preprint arXiv:1310.4283, 2013 | 5 | 2013 |
Evaluating linear functions to symmetric monoidal categories JP Bernardy, A Spiwack Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell, 14-26, 2021 | 4 | 2021 |
A proof of strong normalisation using domain theory. Logic. Methods Comput T Coquand, A Spiwack Science 3 (4), 2007 | 4 | 2007 |
Union and intersection contracts are hard, actually T Freund, Y Hamdaoui, A Spiwack Proceedings of the 17th ACM SIGPLAN International Symposium on Dynamic …, 2021 | 3 | 2021 |
Verified Computation in Homological Algebra A Spiwack | 3* | 2011 |