- Presentation of the work done at Trusted Logic. Brief introduction to
- the Common Criteria Software: lot of documentation must be produced for
- third (and fourth!) parties evaluation; formal evaluation is one goal
- (not yet reached). The main problems Trusted Logic meets are:
- <ul>
- <li>Presentation</li>
- <li>Managing thousands of definitions/theorems and links between them</li>
- <li>Evaluators needs: hiding/displaying information; different views on the
- same proofs/definitions; metadata; backpointers (which lemmas are
- used in a theorem)</li>
- <li>Interoperability with other software tools</li>
- <li>Proofs mantainance</li>
- </ul>
- A final remark is that Trusted Logic is just interested in provability
- (and proof-scripts) and not in proofs (i.e. lambda-terms or natural
- language description of them).
+ <description>
+ Presentation of the work done at Trusted Logic. Brief introduction to
+ the Common Criteria Software: lot of documentation must be produced for
+ third (and fourth!) parties evaluation; formal evaluation is one goal
+ (not yet reached). The main problems Trusted Logic meets are:
+ <ul>
+ <li>Presentation</li>
+ <li>Managing thousands of definitions/theorems and links between them</li>
+ <li>Evaluators needs: hiding/displaying information; different views on the
+ same proofs/definitions; metadata; backpointers (which lemmas are
+ used in a theorem)</li>
+ <li>Interoperability with other software tools</li>
+ <li>Proofs mantainance</li>
+ </ul>
+ A final remark is that Trusted Logic is just interested in provability
+ (and proof-scripts) and not in proofs (i.e. lambda-terms or natural
+ language description of them).
+ </description>