Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

16 résultats
Page :
triés par
Image document

Extending FeatherTrait Java with Interfaces

 Luigi Liquori , Arnaud Spiwack
Theoretical Computer Science, 2008, Theoretical Computer Science, 30 (1-3), pp.243-260. ⟨10.1016/j.tcs.2008.01.051⟩
Article dans une revue inria-00432540v1
Image document

A Proof of Strong Normalisation Using Domain Theory

 Thierry Coquand , Arnaud Spiwack
Logical Methods in Computer Science, 2007, 16 p. ⟨10.2168/LMCS-3(4:12)2007⟩
Article dans une revue inria-00432448v1
Image document

The Rooster and the Syntactic Bracket

 Hugo Herbelin , Arnaud Spiwack
19th International Conference on Types for Proofs and Programs (TYPES 2013), Jul 2014, Toulouse, France. pp.169--187, ⟨10.4230/LIPIcs.TYPES.2013.169⟩
Communication dans un congrès hal-01097919v1
Image document

Extending Coq with Imperative Features and its Application to SAT Verification

 Michaël Armand , Benjamin Grégoire , Arnaud Spiwack , Laurent Théry
Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès inria-00502496v2

Coq 8.4 Reference Manual

 Pierre Boutillier , Stephane Glondu , Benjamin Grégoire , Hugo Herbelin , Pierre Letouzey , et al.
[Research Report] Inria. 2014
Rapport hal-01114602v1
Image document

Linear Haskell: practical linearity in a higher-order polymorphic language

 Jean-Philippe Bernardy , Mathieu Boespflug , Ryan R. Newton , Simon Peyton Jones , Arnaud Spiwack
Proceedings of the ACM on Programming Languages, 2017, 2 (POPL), pp.1-29. ⟨10.1145/3158093⟩
Article dans une revue hal-01673536v1
Image document

An abstract type for constructing tactics in Coq

 Arnaud Spiwack
Proof Search in Type Theory, Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès inria-00502500v1
Image document

Balancing Lists: A Proof Pearl

 Guyslain Naves , Arnaud Spiwack
5th International Conference, ITP 2014, Jul 2014, Vienna, Austria. pp.437 - 449, ⟨10.1007/978-3-319-08970-6_28⟩
Communication dans un congrès hal-01097937v1
Image document

Verified Computing in Homological Algebra

 Arnaud Spiwack
Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English. ⟨NNT : ⟩
Thèse pastel-00605836v1
Image document

Circuits via topoi

 Arnaud Spiwack
[Technical Report] E/421/CRI, Mines ParisTech - PSL Research University - Centre de Recherche en Informatique (CRI). 2015
Rapport hal-01537455v1
Image document

Featherweight-Trait Java : A Trait-based Extension for FJ

 Luigi Liquori , Arnaud Spiwack
[Research Report] RR-5247, INRIA Sophia Antipolis - Méditerranée; INRIA. 2004, pp.27
Rapport inria-00070751v1
Image document

A Proof of Strong Normalisation using Domain Theory

 Thierry Coquand , Arnaud Spiwack
LICS 2006, Aug 2006, Seatle, United States. 10 p., ⟨10.1109/LICS.2006.8⟩
Communication dans un congrès inria-00432490v1
Image document

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, Sep 2008, Hertfordshire, United Kingdom. 21 p
Communication dans un congrès inria-00432575v1
Image document

FeatherTrait: A Modest Extension of Featherweight Java

 Luigi Liquori , Arnaud Spiwack
ACM Transactions on Programming Languages and Systems (TOPLAS), 2008, ACM Transactions on Programming Languages and Systems (TOPLAS), 30 (2), pp.11:1--11:32. ⟨10.1145/1330017.1330022⟩
Article dans une revue inria-00432538v1
Image document

Constructively Finite?

 Arnaud Spiwack , Thierry Coquand
Lambán Pardo, Laureano and Romero Ibáñez, Ana and Rubio García, Julio. Contribuciones científicas en honor de Mirian Andrés Gómez, Universidad de La Rioja, pp.217-230, 2010, 978-84-96487-50-5
Chapitre d'ouvrage inria-00503917v1
Image document

Towards Constructive Homological Algebra in Type Theory

 Thierry Coquand , Arnaud Spiwack
CALCULEMUS 2007, Jun 2007, Hagenberg, Austria. 12 p., ⟨10.1007/978-3-540-73086-6_4⟩
Communication dans un congrès inria-00432525v1
Page :