105 results  save search


...
inria-00000963v1  Conference papers
Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant
33rd Symposium Principles of Programming Languages (POPL 2006), Jan 2006, Charleston, SC, United States. pp.42--54, ⟨10.1145/1111037.1111042⟩
...
hal-00703441v1  Reports
Xavier LeroyAndrew AppelSandrine BlazyGordon Stewart. The CompCert Memory Model, Version 2
[Research Report] RR-7987, INRIA. 2012, pp.26
hal-01350287v1  Journal articles
Xavier Leroy. Comment faire confiance à un compilateur ?
Interstices, INRIA, 2010
...
hal-01059423v1  Conference papers
Xavier Leroy. Formal proofs of code generation and verification tools
SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. pp.1-4, ⟨10.1007/978-3-319-10431-7_1⟩
...
inria-00289540v1  Conference papers
Jean-Baptiste TristanXavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations
35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩
...
inria-00289543v1  Conference papers
Andrew W. AppelXavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract)
Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. pp.95-108, ⟨10.1016/j.entcs.2007.01.020⟩
...
inria-00289545v1  Conference papers
Xavier Leroy. Coinductive big-step operational semantics
European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. pp.42-54, ⟨10.1007/11693024_5⟩
...
inria-00289541v1  Conference papers
Zaynah DargayeXavier Leroy. Mechanized verification of CPS transformations
Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, Oct 2007, Erevan, Armenia. pp.211-225, ⟨10.1007/978-3-540-75560-9_17⟩
...
inria-00289549v1  Conference papers
Yves BertotBenjamin GrégoireXavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis
Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. pp.66-81, ⟨10.1007/11617990⟩
...
inria-00352524v1  Journal articles
Sandrine BlazyXavier Leroy. Mechanized semantics for the Clight subset of the C language
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩
...
inria-00360768v3  Journal articles
Xavier Leroy. A formally verified compiler back-end
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩
...
hal-00862689v3  Journal articles
Sylvie BoldoJacques-Henri JourdanXavier LeroyGuillaume Melquiond. Verified Compilation of Floating-Point Computations
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
...
hal-00674176v1  Journal articles
Andrew AppelRobert DockinsXavier Leroy. A list-machine benchmark for mechanized metatheory
Journal of Automated Reasoning, Springer Verlag, 2012, 49 (3), pp.453--491. ⟨10.1007/s10817-011-9226-1⟩
...
hal-01499939v1  Journal articles
Xavier Leroy. Java bytecode verification: algorithms and formalizations
Journal of Automated Reasoning, Springer Verlag, 2003, 30 (3-4), pp.235--269. ⟨10.1023/A:1025055424017⟩
...
inria-00309010v1  Journal articles
Xavier LeroyHervé Grall. Coinductive big-step operational semantics
Information and Computation, Elsevier, 2009, 207 (2), pp.284-304. ⟨10.1016/j.ic.2007.12.004⟩
...
inria-00529836v1  Conference papers
Jean-Baptiste TristanXavier Leroy. A simple, verified validator for software pipelining
37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. ⟨10.1145/1706299.1706311⟩
...
inria-00529848v1  Book sections
Xavier Leroy. Mechanized semantics
J. Esparza and B. Spanfelner and O. Grumberg. Logics and languages for reliability and security, 25, IOS Press, pp.195-224, 2010, NATO Science for Peace and Security Series D: Information and Communication Security, ⟨10.3233/978-1-60750-100-8-195⟩
...
inria-00529841v1  Conference papers
Silvain RideauXavier Leroy. Validating register allocation and spilling
Compiler Construction 2010, Mar 2010, Paphos, Cyprus. pp.224-243, ⟨10.1007/978-3-642-11970-5_13⟩
...
hal-00981212v1  Conference papers
Robbert KrebbersXavier LeroyFreek Wiedijk. Formal C semantics: CompCert and the C standard
ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. pp.543-548, ⟨10.1007/978-3-319-08970-6_36⟩
...
inria-00106401v1  Conference papers
Sandrine BlazyZaynah DargayeXavier Leroy. Formal Verification of a C Compiler Front-end
FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩
...
inria-00075071v1  Reports
Xavier LeroyMichel Mauny. Dynamics in ML
[Research Report] RR-1491, INRIA. 1991
...
hal-00674663v1  Conference papers
Tahina RamananandroGabriel dos ReisXavier Leroy. A mechanized semantics for C++ object construction and destruction, with applications to resource management
POPL '12 - 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, Jan 2012, Philadelphia, PA, United States. pp.521-532, ⟨10.1145/2103656.2103718⟩
...
hal-01077321v1  Conference papers
Jacques-Henri JourdanFrançois PottierXavier Leroy. Validating LR(1) Parsers
ESOP 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⟩
...
hal-01499972v1  Journal articles
Xavier LeroyMichel Mauny. Dynamics in ML
Journal of Functional Programming, Cambridge University Press (CUP), 1993, 3 (4), pp.431-463. ⟨10.1017/S0956796800000848⟩