equal
deleted
inserted
replaced
272 formalization of a fragment of Java, together with a corresponding virtual |
272 formalization of a fragment of Java, together with a corresponding virtual |
273 machine and a specification of its bytecode verifier and a lightweight |
273 machine and a specification of its bytecode verifier and a lightweight |
274 bytecode verifier, including proofs of type-safety. |
274 bytecode verifier, including proofs of type-safety. |
275 |
275 |
276 This represents a very ``realistic'' example of large formalizations |
276 This represents a very ``realistic'' example of large formalizations |
277 performed in either form of legacy scripts, tactic emulation scripts, and |
277 performed in form of tactic emulation scripts and proper Isar proof texts. |
278 proper Isar proof texts. |
|
279 \end{itemize} |
278 \end{itemize} |
280 |
279 |
281 |
280 |
282 %%% Local Variables: |
281 %%% Local Variables: |
283 %%% mode: latex |
282 %%% mode: latex |