253 typical mathematics-style reasoning in ``axiomatic'' structures. |
253 typical mathematics-style reasoning in ``axiomatic'' structures. |
254 \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a |
254 \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a |
255 big mathematics application on infinitary vector spaces and functional |
255 big mathematics application on infinitary vector spaces and functional |
256 analysis. |
256 analysis. |
257 \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental |
257 \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental |
258 properties of $\lambda$-calculus (Church-Rosser and termination). This may |
258 properties of $\lambda$-calculus (Church-Rosser and termination). |
259 serve as a realistic example of porting of legacy proof scripts into Isar |
259 |
260 tactic emulation scripts. |
260 This may serve as a realistic example of porting of legacy proof scripts |
|
261 into Isar tactic emulation scripts. |
|
262 \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical |
|
263 model of the main aspects of the Unix file-system including its security |
|
264 model, but ignoring processes. A few odd effects caused by the general |
|
265 ``worse-is-better'' approach followed in Unix are discussed within the |
|
266 formal model. |
|
267 |
|
268 This example represents a non-trivial verification task, with all proofs |
|
269 carefully worked out using the proper part of the Isar proof language; |
|
270 unstructured scripts are only used for symbolic evaluation. |
261 \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a |
271 \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a |
262 formalization of a fragment of Java, together with a corresponding virtual |
272 formalization of a fragment of Java, together with a corresponding virtual |
263 machine and a specification of its bytecode verifier and a lightweight |
273 machine and a specification of its bytecode verifier and a lightweight |
264 bytecode verifier, including proofs of type-safety. This represents a very |
274 bytecode verifier, including proofs of type-safety. |
265 ``realistic'' example of large formalizations performed in either form of |
275 |
266 legacy scripts, tactic emulation scripts, and proper Isar proof texts. |
276 This represents a very ``realistic'' example of large formalizations |
|
277 performed in either form of legacy scripts, tactic emulation scripts, and |
|
278 proper Isar proof texts. |
267 \end{itemize} |
279 \end{itemize} |
268 |
280 |
269 |
281 |
270 %%% Local Variables: |
282 %%% Local Variables: |
271 %%% mode: latex |
283 %%% mode: latex |