Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp01zw12z817f
DC FieldValueLanguage
dc.contributor.authorSavary Bélanger, Olivier-
dc.contributor.otherComputer Science Department-
dc.date.accessioned2019-12-03T05:08:32Z-
dc.date.available2019-12-03T05:08:32Z-
dc.date.issued2019-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/dsp01zw12z817f-
dc.description.abstractInteractive theorem provers allow for the development, in the same environment, of programs and of proofs about them. The programmatic portion of the development can then be extracted to code which is then compiled into an executable. However, unless both the extraction and compilation processes are formally verified, one has no guarantees that the proofs developed still apply to the resulting executable. This thesis describes my work on CertiCoq, a verified extraction pipeline for the Coq theorem prover composing with the CompCert C verified compiler to achieve end-to-end correctness guarantees. I present a proof framework to prove optimizations over the continuation-passing style (CPS) intermediate representation (IR) used in CertiCoq. This framework has been used by me and others to prove the correctness of nontrivial optimizations. I focus on a novel proof of correctness for a shrink reduction algorithm, a transformation combining in a single pass multiple optimizations which always result in smaller terms. I also present a verified code generation translating the CPS IR into Clight, a front-end language of CompCert. I show how it interfaces with a verified garbage collector and how its proof composes with the proof of correctness of CompCert. Taken together, this thesis shows how carefully crafted intermediate languages facilitate verification effort in the context of an optimizing compiler.-
dc.language.isoen-
dc.publisherPrinceton, NJ : Princeton University-
dc.relation.isformatofThe Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog: <a href=http://catalog.princeton.edu> catalog.princeton.edu </a>-
dc.subjectCompilers-
dc.subjectExtraction-
dc.subjectFormal software verification-
dc.subjectFunctional Languages-
dc.subjectProgram verification-
dc.subject.classificationComputer science-
dc.titleVerified Extraction for Coq-
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat