Filtrer vos résultats
- 101
- 14
- 60
- 24
- 17
- 3
- 3
- 2
- 2
- 2
- 1
- 1
- 11
- 114
- 1
- 1
- 1
- 1
- 1
- 5
- 1
- 1
- 1
- 3
- 3
- 3
- 1
- 3
- 6
- 1
- 7
- 5
- 5
- 7
- 3
- 3
- 9
- 3
- 1
- 4
- 4
- 3
- 2
- 2
- 5
- 1
- 2
- 3
- 2
- 4
- 3
- 3
- 5
- 102
- 10
- 2
- 1
- 86
- 15
- 12
- 12
- 7
- 7
- 5
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 115
- 11
- 7
- 5
- 4
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
115 résultats
Comment faire confiance à un compilateur ?Interstices, 2010
Article dans une revue
hal-01350287v1
|
|||
|
Towards Formally Verified Optimizing Compilation in Flight Control SoftwarePPES 2011: Predictability and Performance in Embedded Systems, Mar 2011, Grenoble, France. pp.59-68, ⟨10.4230/OASIcs.PPES.2011.59⟩
Communication dans un congrès
inria-00551370v1
|
||
|
Compilation of extended recursion in call-by-value functional languagesPPDP '03, 2003, Uppsala, Sweden. pp.160--171, ⟨10.1145/888251.888267⟩
Communication dans un congrès
hal-00310121v1
|
||
|
A formally verified compiler back-endJournal of Automated Reasoning, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩
Article dans une revue
inria-00360768v3
|
||
|
Well-founded recursion done rightCoqPL 2024: The Tenth International Workshop on Coq for Programming Languages, ACM, Jan 2024, London, United Kingdom
Communication dans un congrès
hal-04356563v2
|
||
|
The effectiveness of type-based unboxingTIC 1997: Workshop Types in Compilation, Jun 1997, Amsterdam, Netherlands
Communication dans un congrès
hal-01499964v1
|
||
|
Dynamics in MLJournal of Functional Programming, 1993, 3 (4), pp.431-463. ⟨10.1017/S0956796800000848⟩
Article dans une revue
istex
hal-01499972v1
|
||
|
A verified framework for higher-order uncurrying optimizationsHigher-Order and Symbolic Computation, 2009, 22 (3), ⟨10.1007/s10990-010-9050-z⟩
Article dans une revue
hal-01499915v1
|
||
|
Parallel Functional Programming with Skeletons: the OCamlP3L experimentACM Workshop on ML and its applications, ACM, Sep 1998, Baltimore, United States
Communication dans un congrès
hal-01499962v1
|
||
|
Verified Code Generation for the Polyhedral ModelProceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.40:1-40:24. ⟨10.1145/3434321⟩
Article dans une revue
hal-03000244v1
|
||
|
Dynamics in ML[Research Report] RR-1491, INRIA. 1991
Rapport
inria-00075071v1
|
||
|
A syntactic theory of type generativity and sharing[Research Report] RR-2545, INRIA. 1995
Rapport
inria-00074133v1
|
||
|
A locally nameless solution to the POPLmark challenge[Research Report] RR-6098, INRIA. 2007, pp.54
Rapport
inria-00123945v2
|
||
|
Formal verification of translation validators: A case study on instruction scheduling optimizations35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩
Communication dans un congrès
inria-00289540v1
|
||
|
Comment faire confiance à un compilateur ?Les Cahiers de l'INRIA - La Recherche, 2010, Cancer la révolution, 440 avril 2010
Article dans une revue
inria-00511377v1
|
||
|
Security properties of typed appletsJan Vitek; Christian D. Jensen Secure Internet Programming - Security issues for Mobile and Distributed Objects, 1603, Springer, pp.147-182, 1999, LNCS, 978-3-540-66130-6. ⟨10.1007/3-540-48749-2_7⟩
Chapitre d'ouvrage
hal-01499957v1
|
||
News from the EDOS project: improving the maintenance of free software distributions.Apr 2006, Porto Alegre, Brazil. pp.199-207
Communication dans un congrès
hal-00154357v1
|
|||
|
Software, between mind and matterCollège de France, 2020, Inaugural lecture at Collège de France
Ouvrages
hal-02392159v2
|
||
|
A simple, verified validator for software pipelining37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. ⟨10.1145/1706299.1706311⟩
Communication dans un congrès
inria-00529836v1
|
||
|
Java bytecode verification: algorithms and formalizationsJournal of Automated Reasoning, 2003, 30 (3-4), pp.235--269. ⟨10.1023/A:1025055424017⟩
Article dans une revue
istex
hal-01499939v1
|
||
|
CamlDimLogiciel hal-01863457v1 |
||
Déchiffrement(s) : des hiéroglyphes à l’ADNOdile Jacob, pp.272, 2023, Colloque annuel du Collège de France, 978-2-415-00687-7
Proceedings/Recueil des communications
hal-04210865v1
|
|||
|
Sciences du logicielL'Annuaire du Collège de France. Résumés des cours et travaux, 2023, 120, pp.13-22. ⟨10.4000/annuaire-cdf.18052⟩
Article dans une revue
hal-04245933v1
|
||
|
Sciences du logicielL'Annuaire du Collège de France. Résumés des cours et travaux, 2022, 119, pp.21-33. ⟨10.4000/annuaire-cdf.16737⟩
Article dans une revue
hal-04265123v1
|
||
|
CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing CompilerERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9
Communication dans un congrès
hal-01643290v1
|
||
|
Formal Verification of a C Compiler Front-endFM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩
Communication dans un congrès
inria-00106401v1
|
||
|
Validating LR(1) ParsersESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. pp.397-416, ⟨10.1007/978-3-642-28869-2_20⟩
Communication dans un congrès
hal-01077321v1
|
||
|
A list-machine benchmark for mechanized metatheory[Research Report] RR-5914, INRIA. 2006
Rapport
inria-00077531v1
|
||
|
A Formally-Verified C Compiler Supporting Floating-Point ArithmeticArith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115
Communication dans un congrès
hal-00743090v2
|
||
|
Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves2007
Pré-publication, Document de travail
inria-00176007v1
|