Mostly sound type system improves a foundational program verifier
Author(s): Dodds, J; Appel, Andrew W.
DownloadTo refer to this page use:
http://arks.princeton.edu/ark:/88435/pr1hw2kFull metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor.author | Dodds, J | - |
| dc.contributor.author | Appel, Andrew W. | - |
| dc.date.accessioned | 2016-10-17T14:14:50Z | - |
| dc.date.available | 2016-10-17T14:14:50Z | - |
| dc.date.issued | 2013-12-01 | en_US |
| dc.identifier.citation | Dodds, J, Appel, AW. "Mostly sound type system improves a foundational program verifier" Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8307 LNCS, 17 - 32, doi:10.1007/978-3-319-03545-1_2 | en_US |
| dc.identifier.issn | 0302-9743 | - |
| dc.identifier.uri | http://arks.princeton.edu/ark:/88435/pr1hw2k | - |
| dc.description.abstract | We integrate a verified typechecker with a verified program logic for the C language, proved sound with respect to the operational semantics of the CompCert verified optimizing C compiler. The C language is known to not be type-safe but we show the value of a provably mostly sound type system: integrating the typechecker with the program logic makes the logic significantly more usable. The computational nature of our typechecker (within Coq) makes program proof much more efficient. We structure the system so that symbolic execution - even tactical (nonreflective) symbolic execution - can keep the type context and typechecking always in reified form, to avoid expensive re-reification. © Springer International Publishing 2013. | en_US |
| dc.format.extent | 17 - 32 | en_US |
| dc.relation.ispartof | Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013 | en_US |
| dc.relation.ispartofseries | Lecture Notes in Computer Science; | - |
| dc.rights | This is the author’s final manuscript. All rights reserved to author(s). | en_US |
| dc.title | Mostly sound type system improves a foundational program verifier | en_US |
| dc.type | Conference Article | en_US |
| dc.identifier.doi | doi:10.1007/978-3-319-03545-1_2 | - |
| dc.identifier.eissn | 1611-3349 | - |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| AppelCPP2013.pdf | 304.52 kB | Adobe PDF | View/Download |
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.