Foundational proof-carrying code

By A. Appel. Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, 2001

379 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

RustBelt: securing the foundations of the rust programming language (2017, methodology): “Moreover, thanks to the Foundational Proof-Carrying Code project [Ahmed et al. 2010; Appel 2001] and the development of łstep-indexedž logical relations [Ahmed 2004; Appel and McAllester 2001] which arose from that project, we now know how to scale the semantic approach to languages with…”
Proof carrying code (2015, background): “[2] VCGen requires that the agent code is syntactically well formed in the selected language, all functions defined and used internally by the agent code are annotated with a precondition and a post-condition, and also that”
A Formally Verified Compiler Back-end (2009, background): “The proof-carrying code (PCC) approach [75,2,33] does not attempt to establish semantic preservation between a source program and some compiled code.”
Formal verification of a realistic compiler (2009, background): “Therefore, establishing property (2) once and for all spares us from establishing property (4) for every speciﬁcation of interest.”
Mechanized Metatheory for the Masses: The PoplMark Challenge (2005, background): “Some other significant existing applications of mechanized metatheory include Foundational Proof Carrying Code [1] and Typed Assembly Languages [4].”