Next: University of Durham Up: Progress Report Previous: University of Birmingham

Univiversity of Cambridge

Cambridge contributed to Isabelle99, which was released on 3 November 1999. Items developed at Cambridge include (1) a sound and generic treatment of literal arithmetic, which is applied to the natural numbers, integers and reals, (2) a theory of non-standard analysis and (3) a link-up to a decision procedure package, the Stanford Validity Checker. Cambridge continued its investigations into the semantics and mechanization of the UNITY formalism. The focus of attention is compositionality: principles to allow properties of a system to be derived from the properties of its parts. A paper on this work is accepted to the ACM Transactions on Computational Logic.

Publication

Mechanizing UNIT} in Isabelle by Lawrence C. Paulson, TOCL. In press



Next: University of Durham Up: Progress Report Previous: University of Birmingham