 |
 |
 |
|
|
||
|---|---|---|
|
inria-00000963v1
Conference papers
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
The CompCert Memory Model, Version 2 [Research Report] RR-7987, INRIA. 2012, pp.26 |
||
|
hal-00154357v1
Conference papers
News from the EDOS project: improving the maintenance of free software distributions. Apr 2006, Porto Alegre, Brazil. pp.199-207 |
||
|
hal-00154188v1
Conference papers
Maintaining large software distributions: new challenges from the FOSS era. Apr 2006, Vienna, Austria. pp.7-20 |
||
|
hal-01059423v1
Conference papers
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
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
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
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
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
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
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
A formally verified compiler back-end Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩ |
||
|
inria-00289709v1
Journal articles
Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩ |
||
|
hal-00862689v3
Journal articles
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
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⟩ |
||
|
inria-00289542v1
Journal articles
Formal verification of a C-like memory model and its uses for verifying program transformations Journal of Automated Reasoning, Springer Verlag, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩ |
||
|
hal-01499939v1
Journal articles
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
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
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
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
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
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
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⟩ |
||
|
|
||
|
hal-00674663v1
Conference papers
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
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⟩ |
||
|
inria-00071903v1
Reports
A reduction semantics for call-by-value mixin modules [Research Report] RR-4682, INRIA. 2002 |
||
|
hal-01499972v1
Journal articles
Dynamics in ML Journal of Functional Programming, Cambridge University Press (CUP), 1993, 3 (4), pp.431-463. ⟨10.1017/S0956796800000848⟩ |
||
|
|
||
