Proof-Carrying Components (PCC) are a form of trusted components, for which the guarantee of quality is perhaps the strongest one possible: a mathematical proof, machine-checkable, that the component satisfies specific properties, known as the contract for the component. These properties can be more or less extensive: they might characterize all that's interesting about the component's behavior, or just some specific aspects, such as absence of "null-pointer dereferencing" or other run-time failures.
Proof-Carrying Components can be automatically generated using Proof-Transforming Compilers. PTCs are similar to certifying compilers in PCC, but take a source proof as input and produce the bytecode proof. An important property of Proof-Transforming Compilers is that they do not have to be trusted. If the compiler produces a wrong specification or a wrong proof for a component, the proof checker will reject the component.
To show the feasibility of Proof-Transforming Compilers, Nordio, Karahan, Guex and Hess have implemented a PTC for a subset of Eiffel. The compiler takes a proof of an Eiffel program in XML format and produces the bytecode proof. However, the bytecode proof produced as result is not embedded in any theorem prover.
This project consists of embedding the Proof-Carrying Components into Isabelle. The components are automatically generated by the PTC. The compiler produces an AST of the component. The goal of this project is embedding the component into Isabelle.