Changeset 3650


Ignore:
Timestamp:
Mar 13, 2017, 7:58:47 PM (12 days ago)
Author:
mulligan
Message:

Finished first draft of verified compilation subsection. Many new references/citations.

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.bib

    r3649 r3650  
    1616  pages     = {270--281},
    1717  year      = {2014},
    18   crossref  = {DBLP:conf/pldi/2014},
    1918  url       = {http://doi.acm.org/10.1145/2594291.2594301},
    2019  doi       = {10.1145/2594291.2594301},
     
    3938}
    4039
    41 
     40@inproceedings{Tristan-Leroy-LCM,
     41  author = {Jean-Baptiste Tristan and Xavier Leroy},
     42  title = {Verified Validation of {Lazy} {Code} {Motion}},
     43  booktitle = {Proceedings of the 2009 ACM SIGPLAN Conference on
     44                         Programming Language Design and Implementation
     45                         (PLDI'09)},
     46  year = 2009,
     47  pages = {316--326},
     48  url = {http://gallium.inria.fr/~xleroy/publi/validation-LCM.pdf},
     49  urlpublisher = {http://doi.acm.org/10.1145/1542476.1542512},
     50  hal = {http://hal.archives-ouvertes.fr/inria-00415865/},
     51  pubkind = {conf-int-mono}
     52}
     53
     54@incollection{Leroy-Appel-Blazy-Stewart-memory,
     55  author = {Leroy, Xavier and Appel, Andrew W. and Blazy, Sandrine and Stewart, Gordon},
     56  title = {The {CompCert} memory model},
     57  year = {2014},
     58  month = apr,
     59  booktitle = {Program Logics for Certified Compilers},
     60  editor = {Appel, Andrew W.},
     61  publisher = {Cambridge University Press},
     62  url = {http://vst.cs.princeton.edu/}
     63}
     64
     65@article{Sevcik:2013:CVC:2487241.2487248,
     66 author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
     67 title = {CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency},
     68 journal = {J. ACM},
     69 issue_date = {June 2013},
     70 volume = {60},
     71 number = {3},
     72 month = jun,
     73 year = {2013},
     74 issn = {0004-5411},
     75 pages = {22:1--22:50},
     76 articleno = {22},
     77 numpages = {50},
     78 url = {http://doi.acm.org/10.1145/2487241.2487248},
     79 doi = {10.1145/2487241.2487248},
     80 acmid = {2487248},
     81 publisher = {ACM},
     82 address = {New York, NY, USA},
     83 keywords = {Relaxed memory models, semantics, verified compilation},
     84}
     85
     86@article{Kang:2016:LVS:2914770.2837642,
     87 author = {Kang, Jeehoon and Kim, Yoonseung and Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor},
     88 title = {Lightweight Verification of Separate Compilation},
     89 journal = {SIGPLAN Not.},
     90 issue_date = {January 2016},
     91 volume = {51},
     92 number = {1},
     93 month = jan,
     94 year = {2016},
     95 issn = {0362-1340},
     96 pages = {178--190},
     97 numpages = {13},
     98 url = {http://doi.acm.org/10.1145/2914770.2837642},
     99 doi = {10.1145/2914770.2837642},
     100 acmid = {2837642},
     101 publisher = {ACM},
     102 address = {New York, NY, USA},
     103 keywords = {CompCert, Compositional compiler verification, separate compilation},
     104}
     105
     106@article{Stewart:2015:CC:2775051.2676985,
     107 author = {Stewart, Gordon and Beringer, Lennart and Cuellar, Santiago and Appel, Andrew W.},
     108 title = {Compositional CompCert},
     109 journal = {SIGPLAN Not.},
     110 issue_date = {January 2015},
     111 volume = {50},
     112 number = {1},
     113 month = jan,
     114 year = {2015},
     115 issn = {0362-1340},
     116 pages = {275--287},
     117 numpages = {13},
     118 url = {http://doi.acm.org/10.1145/2775051.2676985},
     119 doi = {10.1145/2775051.2676985},
     120 acmid = {2676985},
     121 publisher = {ACM},
     122 address = {New York, NY, USA},
     123 keywords = {compcert, compiler correctness},
     124}
     125
     126@inproceedings{Boldo-Jourdan-Leroy-Melquiond-2013,
     127  title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
     128  author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
     129  booktitle = {ARITH, 21st IEEE International Symposium on Computer Arithmetic},
     130  pages = {107-115},
     131  publisher = {IEEE Computer Society Press},
     132  url = {http://hal.inria.fr/hal-00743090},
     133  year = 2013,
     134  xtopic = {compcert},
     135  abstract = {Floating-point arithmetic is known to be tricky: roundings, formats,
     136exceptional values. The IEEE-754 standard was a push towards
     137straightening the field and made formal reasoning about floating-point
     138computations easier and flourishing. Unfortunately, this is not
     139sufficient to guarantee the final result of a program, as several
     140other actors are involved: programming language, compiler,
     141architecture.  The CompCert formally-verified compiler provides a
     142solution to this problem: this compiler comes with a mathematical
     143specification of the semantics of its source language (a large subset
     144of ISO C90) and target platforms (ARM, PowerPC, x86-SSE2), and with a
     145proof that compilation preserves semantics.  In this paper, we report
     146on our recent success in formally specifying and proving correct
     147CompCert's compilation of floating-point arithmetic.  Since CompCert
     148is verified using the Coq proof assistant, this effort required a
     149suitable Coq formalization of the IEEE-754 standard; we extended the
     150Flocq library for this purpose.  As a result, we obtain the first
     151formally verified compiler that provably preserves the semantics of
     152floating-point programs.}
     153}
     154
     155@inproceedings{2006-Leroy-Bertot-Gregoire,
     156  author = {Yves Bertot and Benjamin Grégoire and Xavier Leroy},
     157  title = {A structured approach to proving compiler
     158                         optimizations based on dataflow analysis},
     159  booktitle = {Types for Proofs and Programs, Workshop TYPES 2004},
     160  year = 2006,
     161  volume = 3839,
     162  pages = {66-81},
     163  series = {Lecture Notes in Computer Science},
     164  publisher = {Springer},
     165  url = {http://gallium.inria.fr/~xleroy/publi/proofs_dataflow_optimizations.pdf},
     166  urlpublisher = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11617990_5},
     167  hal = {http://hal.inria.fr/inria-00289549/},
     168  abstract = {
     169This paper reports on the correctness proof of compiler optimizations
     170based on data-flow analysis.  We formulate the optimizations and
     171analyses as instances of a general framework for data-flow analyses and
     172transformations, and prove that the optimizations preserve the
     173behavior of the compiled programs.  This development is a part of a
     174larger effort of certifying an optimizing compiler by proving semantic
     175equivalence between source and compiled code.}
     176}
     177
     178@inproceedings{Robert-Leroy-2012,
     179  author = {Valentin Robert and Xavier Leroy},
     180  title = {A Formally-Verified Alias Analysis},
     181  booktitle = {Certified Programs and Proofs (CPP 2012)},
     182  year = 2012,
     183  series = {Lecture Notes in Computer Science},
     184  volume = 7679,
     185  pages = {11-26},
     186  publisher = {Springer},
     187  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-35308-6_5},
     188  url = {http://gallium.inria.fr/~xleroy/publi/alias-analysis.pdf},
     189  xtopic = {compcert},
     190  abstract = {This paper reports on the formalization and proof of soundness, using
     191the Coq proof assistant, of an alias analysis: a static analysis that
     192approximates the flow of pointer values.  The alias analysis
     193considered is of the points-to kind and is intraprocedural,
     194flow-sensitive, field-sensitive, and untyped.  Its soundness proof
     195follows the general style of abstract interpretation.
     196The analysis is designed to fit in the CompCert C verified compiler,
     197supporting future aggressive optimizations over memory accesses.}
     198}
     199
     200@article{LEINENBACH200823,
     201title = "Pervasive Compiler Verification – From Verified Programs to Verified Systems",
     202journal = "Electronic Notes in Theoretical Computer Science",
     203volume = "217",
     204number = "",
     205pages = "23 - 40",
     206year = "2008",
     207note = "",
     208issn = "1571-0661",
     209doi = "http://dx.doi.org/10.1016/j.entcs.2008.06.040",
     210url = "http://www.sciencedirect.com/science/article/pii/S1571066108003836",
     211author = "Dirk Leinenbach and Elena Petrova",
     212keywords = "Compiler Verification",
     213keywords = "Theorem Proving",
     214keywords = "System Verification",
     215keywords = "HOL",
     216keywords = "Hoare Logic"
     217}
     218
     219@inproceedings{DBLP:conf/cpp/MulliganC12,
     220  author    = {Dominic P. Mulligan and
     221               Claudio Sacerdoti Coen},
     222  title     = {On the Correctness of an Optimising Assembler for the Intel {MCS-51}
     223               Microprocessor},
     224  booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
     225               2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
     226  pages     = {43--59},
     227  year      = {2012},
     228  url       = {http://dx.doi.org/10.1007/978-3-642-35308-6_7},
     229  doi       = {10.1007/978-3-642-35308-6_7},
     230  timestamp = {Thu, 08 Nov 2012 16:22:09 +0100},
     231  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/MulliganC12},
     232  bibsource = {dblp computer science bibliography, http://dblp.org}
     233}
     234
     235@inproceedings{DBLP:conf/tacas/BoenderC14,
     236  author    = {Jaap Boender and
     237               Claudio Sacerdoti Coen},
     238  title     = {On the Correctness of a Branch Displacement Algorithm},
     239  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
     240               - 20th International Conference, {TACAS} 2014, Held as Part of the
     241               European Joint Conferences on Theory and Practice of Software, {ETAPS}
     242               2014, Grenoble, France, April 5-13, 2014. Proceedings},
     243  pages     = {605--619},
     244  year      = {2014},
     245  url       = {http://dx.doi.org/10.1007/978-3-642-54862-8_53},
     246  doi       = {10.1007/978-3-642-54862-8_53},
     247  timestamp = {Sun, 23 Mar 2014 11:19:21 +0100},
     248  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/BoenderC14},
     249  bibsource = {dblp computer science bibliography, http://dblp.org}
     250}
     251
     252@article{Dave:2003:CVB:966221.966235,
     253 author = {Dave, Maulik A.},
     254 title = {Compiler Verification: A Bibliography},
     255 journal = {SIGSOFT Softw. Eng. Notes},
     256 issue_date = {November 2003},
     257 volume = {28},
     258 number = {6},
     259 month = nov,
     260 year = {2003},
     261 issn = {0163-5948},
     262 pages = {2--2},
     263 numpages = {1},
     264 url = {http://doi.acm.org/10.1145/966221.966235},
     265 doi = {10.1145/966221.966235},
     266 acmid = {966235},
     267 publisher = {ACM},
     268 address = {New York, NY, USA},
     269}
     270
     271@inproceedings{Myreen:2009:EPC:1532828.1532830,
     272 author = {Myreen, Magnus O. and Slind, Konrad and Gordon, Michael J.},
     273 title = {Extensible Proof-Producing Compilation},
     274 booktitle = {Proceedings of the 18th International Conference on Compiler Construction: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009},
     275 series = {CC '09},
     276 year = {2009},
     277 isbn = {978-3-642-00721-7},
     278 location = {York, UK},
     279 pages = {2--16},
     280 numpages = {15},
     281 url = {http://dx.doi.org/10.1007/978-3-642-00722-4_2},
     282 doi = {10.1007/978-3-642-00722-4_2},
     283 acmid = {1532830},
     284 publisher = {Springer-Verlag},
     285 address = {Berlin, Heidelberg},
     286}
     287
     288@inproceedings{Li:2008:TST:1792734.1792783,
     289 author = {Li, Guodong and Slind, Konrad},
     290 title = {Trusted Source Translation of a Total Function Language},
     291 booktitle = {Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
     292 series = {TACAS'08/ETAPS'08},
     293 year = {2008},
     294 isbn = {3-540-78799-2, 978-3-540-78799-0},
     295 location = {Budapest, Hungary},
     296 pages = {471--485},
     297 numpages = {15},
     298 url = {http://dl.acm.org/citation.cfm?id=1792734.1792783},
     299 acmid = {1792783},
     300 publisher = {Springer-Verlag},
     301 address = {Berlin, Heidelberg},
     302}
     303
     304@inproceedings{Myreen:2009:VLI:1616077.1616105,
     305 author = {Myreen, Magnus O. and Gordon, Michael J.},
     306 title = {Verified LISP Implementations on ARM, x86 and PowerPC},
     307 booktitle = {Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics},
     308 series = {TPHOLs '09},
     309 year = {2009},
     310 isbn = {978-3-642-03358-2},
     311 location = {Munich, Germany},
     312 pages = {359--374},
     313 numpages = {16},
     314 url = {http://dx.doi.org/10.1007/978-3-642-03359-9_25},
     315 doi = {10.1007/978-3-642-03359-9_25},
     316 acmid = {1616105},
     317 publisher = {Springer-Verlag},
     318 address = {Berlin, Heidelberg},
     319}
     320
     321@article{Tatlock:2010:BEV:1809028.1806611,
     322 author = {Tatlock, Zachary and Lerner, Sorin},
     323 title = {Bringing Extensibility to Verified Compilers},
     324 journal = {SIGPLAN Not.},
     325 issue_date = {June 2010},
     326 volume = {45},
     327 number = {6},
     328 month = jun,
     329 year = {2010},
     330 issn = {0362-1340},
     331 pages = {111--121},
     332 numpages = {11},
     333 url = {http://doi.acm.org/10.1145/1809028.1806611},
     334 doi = {10.1145/1809028.1806611},
     335 acmid = {1806611},
     336 publisher = {ACM},
     337 address = {New York, NY, USA},
     338 keywords = {compiler optimization, correctness, extensibility},
     339}
     340
     341@article{Chlipala:2007:CTC:1273442.1250742,
     342 author = {Chlipala, Adam},
     343 title = {A Certified Type-preserving Compiler from Lambda Calculus to Assembly Language},
     344 journal = {SIGPLAN Not.},
     345 issue_date = {June 2007},
     346 volume = {42},
     347 number = {6},
     348 month = jun,
     349 year = {2007},
     350 issn = {0362-1340},
     351 pages = {54--65},
     352 numpages = {12},
     353 url = {http://doi.acm.org/10.1145/1273442.1250742},
     354 doi = {10.1145/1273442.1250742},
     355 acmid = {1250742},
     356 publisher = {ACM},
     357 address = {New York, NY, USA},
     358 keywords = {compiler verification, denotational semantics, dependent types, interactive proof assistants},
     359}
     360
     361@article{Chlipala:2010:VCI:1707801.1706312,
     362 author = {Chlipala, Adam},
     363 title = {A Verified Compiler for an Impure Functional Language},
     364 journal = {SIGPLAN Not.},
     365 issue_date = {January 2010},
     366 volume = {45},
     367 number = {1},
     368 month = jan,
     369 year = {2010},
     370 issn = {0362-1340},
     371 pages = {93--106},
     372 numpages = {14},
     373 url = {http://doi.acm.org/10.1145/1707801.1706312},
     374 doi = {10.1145/1707801.1706312},
     375 acmid = {1706312},
     376 publisher = {ACM},
     377 address = {New York, NY, USA},
     378 keywords = {compiler verification, interactive proof assistants},
     379}
     380
     381@article{Wang:2014:CVM:2714064.2660201,
     382 author = {Wang, Peng and Cuellar, Santiago and Chlipala, Adam},
     383 title = {Compiler Verification Meets Cross-language Linking via Data Abstraction},
     384 journal = {SIGPLAN Not.},
     385 issue_date = {October 2014},
     386 volume = {49},
     387 number = {10},
     388 month = oct,
     389 year = {2014},
     390 issn = {0362-1340},
     391 pages = {675--690},
     392 numpages = {16},
     393 url = {http://doi.acm.org/10.1145/2714064.2660201},
     394 doi = {10.1145/2714064.2660201},
     395 acmid = {2660201},
     396 publisher = {ACM},
     397 address = {New York, NY, USA},
     398 keywords = {abstract data types, compiler verification, cross-language linking, program logics},
     399}
     400
     401@article{KLEIN200427,
     402title = "Verified bytecode verification and type-certifying compilation",
     403journal = "The Journal of Logic and Algebraic Programming",
     404volume = "58",
     405number = "1",
     406pages = "27 - 60",
     407year = "2004",
     408note = "",
     409issn = "1567-8326",
     410doi = "http://dx.doi.org/10.1016/j.jlap.2003.07.004",
     411url = "http://www.sciencedirect.com/science/article/pii/S1567832603000754",
     412author = "Gerwin Klein and Martin Strecker",
     413keywords = "Java",
     414keywords = "JVM",
     415keywords = "Compiler",
     416keywords = "Bytecode verification",
     417keywords = "Theorem proving"
     418}
     419
     420@Inbook{Strecker2002,
     421author="Strecker, Martin",
     422editor="Voronkov, Andrei",
     423title="Formal Verification of a Java Compiler in Isabelle",
     424bookTitle="Automated Deduction---CADE-18: 18th International Conference on Automated Deduction Copenhagen, Denmark, July 27--30, 2002 Proceedings",
     425year="2002",
     426publisher="Springer Berlin Heidelberg",
     427address="Berlin, Heidelberg",
     428pages="63--77",
     429isbn="978-3-540-45620-9",
     430doi="10.1007/3-540-45620-1_5",
     431url="http://dx.doi.org/10.1007/3-540-45620-1_5"
     432}
     433
     434@article{Kumar:2014:CVI:2578855.2535841,
     435 author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
     436 title = {CakeML: A Verified Implementation of ML},
     437 journal = {SIGPLAN Not.},
     438 issue_date = {January 2014},
     439 volume = {49},
     440 number = {1},
     441 month = jan,
     442 year = {2014},
     443 issn = {0362-1340},
     444 pages = {179--191},
     445 numpages = {13},
     446 url = {http://doi.acm.org/10.1145/2578855.2535841},
     447 doi = {10.1145/2578855.2535841},
     448 acmid = {2535841},
     449 publisher = {ACM},
     450 address = {New York, NY, USA},
     451 keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking},
     452}
     453
     454@inproceedings{Rideau-Leroy-regalloc,
     455  author = {Silvain Rideau and Xavier Leroy},
     456  title = {Validating register allocation and spilling},
     457  booktitle = {Compiler Construction (CC 2010)},
     458  year = 2010,
     459  publisher = {Springer},
     460  series = {Lecture Notes in Computer Science},
     461  volume = 6011,
     462  pages = {224-243},
     463  xtopic = {compcert},
     464  url = {http://gallium.inria.fr/~xleroy/publi/validation-regalloc.pdf},
     465  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
     466  abstract = {Following the translation validation approach to high-assurance
     467compilation, we describe a new algorithm for validating {\em a
     468posteriori} the results of a run of register allocation.  The
     469algorithm is based on backward dataflow inference of
     470equations between variables, registers and stack locations, and can
     471cope with sophisticated forms of spilling and live range splitting, as
     472well as many forms of architectural irregularities such as overlapping
     473registers.  The soundness of the algorithm was mechanically proved
     474using the Coq proof assistant.}
     475}
     476
     477@inproceedings{Blazy-Robillard-splitting,
     478  author = {Sandrine Blazy and Benoît Robillard},
     479  title = {Live-range Unsplitting for Faster Optimal Coalescing},
     480  booktitle = {Proceedings of the ACM SIGPLAN/SIGBED 2009
     481                         conference on Languages,
     482                         Compilers, and Tools for Embedded Systems
     483                         (LCTES 2009)},
     484  pages = {70--79},
     485  publisher = {ACM Press},
     486  year = 2009,
     487  url = {http://www.ensiie.fr/~blazy/LCTES09.pdf},
     488  urlpublisher = {http://doi.acm.org/10.1145/1542452.1542462},
     489  hal = {http://hal.inria.fr/inria-00387749/},
     490  pubkind = {conf-int-mono}
     491}
    42492
    43493@article{Regehr:2005:ESO:1113830.1113833,
     
    71521  pages     = {22--37},
    72522  year      = {2006},
    73   crossref  = {DBLP:conf/esop/2006},
    74523  url       = {http://dx.doi.org/10.1007/11693024_3},
    75524  doi       = {10.1007/11693024_3},
     
    162611url = "http://www.sciencedirect.com/science/article/pii/S0304397507006627",
    163612author = "David Aspinall and Lennart Beringer and Martin Hofmann and Hans-Wolfgang Loidl and Alberto Momigliano",
    164 }
    165 
    166 @inproceedings{DBLP:conf/esop/HofmannJ06,
    167   author    = {Martin Hofmann and
    168                Steffen Jost},
    169   title     = {Type-Based Amortised Heap-Space Analysis},
    170   booktitle = {Programming Languages and Systems, 15th European Symposium on Programming,
    171                {ESOP} 2006, Held as Part of the Joint European Conferences on Theory
    172                and Practice of Software, {ETAPS} 2006, Vienna, Austria, March 27-28,
    173                2006, Proceedings},
    174   pages     = {22--37},
    175   year      = {2006},
    176   crossref  = {DBLP:conf/esop/2006},
    177   url       = {http://dx.doi.org/10.1007/11693024_3},
    178   doi       = {10.1007/11693024_3},
    179   timestamp = {Thu, 28 May 2015 17:23:23 +0200},
    180   biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/HofmannJ06},
    181   bibsource = {dblp computer science bibliography, http://dblp.org}
    182613}
    183614
     
    302733  pages     = {11--20},
    303734  year      = {2014},
    304   crossref  = {DBLP:conf/wcet/2014},
    305735  url       = {http://dx.doi.org/10.4230/OASIcs.WCET.2014.11},
    306736  doi       = {10.4230/OASIcs.WCET.2014.11},
     
    433863  pages     = {178-188},
    434864  ee        = {http://doi.acm.org/10.1145/41625.41641},
    435   crossref  = {DBLP:conf/popl/1987},
    436865  bibsource = {DBLP, http://dblp.uni-trier.de}
    437866}
     
    497926  booktitle = {TFP},
    498927  year      = {2005},
    499   pages     = {195--210},
    500   crossref  = {TFP2005},
     928  pages     = {195--210}
    501929}
    502930
     
    529957  pages     = {298--302},
    530958  year      = {2007},
    531   crossref  = {DBLP:conf/cav/2007},
    532959  url       = {http://dx.doi.org/10.1007/978-3-540-73368-3_34},
    533960  doi       = {10.1007/978-3-540-73368-3_34},
     
    567994  pages     = {64-69},
    568995  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
    569   crossref  = {DBLP:conf/cade/2011},
    570996  bibsource = {DBLP, http://dblp.uni-trier.de}
    571997}
  • Papers/jar-cerco-2017/conclusions.tex

    r3649 r3650  
    104104\paragraph{Verified compilation}
    105105
    106 As a verified compilation project, CerCo is also related to various other verified compilation projects.
     106The CerCo verified C compiler is naturally related to other verified compilation projects (see e.g.~\cite{Kumar:2014:CVI:2578855.2535841,LEINENBACH200823,Strecker2002,KLEIN200427,Wang:2014:CVM:2714064.2660201,Chlipala:2010:VCI:1707801.1706312,Chlipala:2007:CTC:1273442.1250742,Myreen:2009:VLI:1616077.1616105,Li:2008:TST:1792734.1792783,Myreen:2009:EPC:1532828.1532830} for more recent work, and~\cite{Dave:2003:CVB:966221.966235} for a now slightly outdated overview of the field) in that we consider the general problem of proving a program's semantics---whether functional or non-functional---are preserved under compilation, generally construed.
    107107
    108 Perhaps the most closely related verified compiler to our own is the CompCert verified C compiler project~\cite{compcert}.
     108However, out of all verified compiler projects, we view the CompCert verified C compiler~\cite{compcert} as the most closely related verified compiler to our own.
    109109Indeed, the intermediate languages chosen into the CerCo verified C compiler are at least partially inspired by those implemented in the CompCert compiler.
    110 Several differences between the two projects stand out.
     110Several differences between the two projects stand out, however.
     111
    111112Most importantly, the vanilla CompCert compiler does not consider the lifting of any cost model from machine code to the source-level, which we do.
     113Indeed, the correctness theorem for the CompCert compiler focusses exclusively on the preservation of extensional (functional) properties of the program under compilation.
     114Whilst we consider extensional correctness, we also consider the tracking of non-functional properties of the program, too.
     115This focus on lifting a cost model from machine code to high-level source code means that we must consider the generation of machine code, rather than assembly code, from our compiler.
     116Therefore, unlike CompCert, the CerCo C compiler also contains a verified lightly-optimising assembler for our target architecture~\cite{DBLP:conf/tacas/BoenderC14,DBLP:conf/cpp/MulliganC12}.
     117
     118Further, the CompCert verified C compiler, since its initial release, has served as a nexus for research into the verification of realistic C compilers.
     119As a result, various optimisations (e.g.~\cite{Tatlock:2010:BEV:1809028.1806611,Tristan-Leroy-LCM,Rideau-Leroy-regalloc,Blazy-Robillard-splitting}), program analyses (e.g.~\cite{Robert-Leroy-2012,2006-Leroy-Bertot-Gregoire}), extensions to the base CompCert C language and its semantics (e.g.~\cite{Boldo-Jourdan-Leroy-Melquiond-2013,Stewart:2015:CC:2775051.2676985,Kang:2016:LVS:2914770.2837642}), retargettings of the compiler to alternative hardware platforms (e.g.~\cite{Sevcik:2013:CVC:2487241.2487248}), and various program logics (e.g.~\cite{Leroy-Appel-Blazy-Stewart-memory}) have all extended the base CompCert verified compiler.
     120None of this work has been implemented for the CerCo verified C compiler, meaning that CompCert is a much more aggressively optimising compiler, with a better developed toolchain surrounding the compiler, than the verified compiler presented in this paper.
     121
     122Lastly, the implementation styles of the two compilers, and their proofs, differ quite markedly.
     123CompCert was intentionally written using as few indexed families of types, and as few advanced features of the Coq proof assistant, as possible.
     124CerCo, on the other hand, was partially intended to stress-test the Matita type checker and reduction machinery, and also intended as a project that would explore the design space of verified compilers in a dependently-typed proof assistant.
     125As a result, the Cerco implementation and proof of correctness makes extensive use of indexed type families and dependent types.
    112126
    113127% CompCert, CompCertTSO, CakeML, C0, etc.
Note: See TracChangeset for help on using the changeset viewer.