Name
Abstract | ||
|---|---|---|
This paper presents the initial results of a project to determine ifthe techniques of proof-carrying code and certifying compilers can be applied to programming languages of realistic size and complexity. The experiment shows that: (1) it is possible to implement a certifying native-code compiler for a large subset of the Java programming language; (2) the compiler is freely able to apply many standard local and global optimizations; and (3) the PCC binaries it produces are of reasonable size and can be rapidly checked for type safety by a small proof-checker. This paper also presents further evidence that PCC provides several advantages for compiler development. In particular, generating proofs of the target code helps to identify compiler bugs, many of which would have been difficult to discover by testing. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1145/349299.349315 | PLDI '02 Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation |
Keywords | Field | DocType |
type safety,programming language,virtual machine,compression,global optimization | Dead code elimination,Inline expansion,Interprocedural optimization,Dynamic compilation,Programming language,Functional compiler,Computer science,Compiler correctness,Theoretical computer science,Compiler,Compiler construction | Conference |
Volume | Issue | ISSN |
35 | 5 | 0362-1340 |
ISBN | Citations | PageRank |
1-58113-199-2 | 93 | 6.77 |
References | Authors | |
7 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christopher Colby | 1 | 237 | 18.39 |
| Peter Lee 0001 | 2 | 975 | 147.71 |
| George Necula | 3 | 2427 | 180.97 |
| Fred Blau | 4 | 93 | 6.77 |
| Mark Plesko | 5 | 184 | 13.81 |
| Kenneth Cline | 6 | 93 | 6.77 |