B. Glossary

CESG

Communications and Electronic Security Group (a part of GCHQ).

class

A `large' collection.

GCHQ

Government Communications Headquarters, UK.

HOL

Higher Order Logic, a specification language, a formal deductive logic, an interactive proof tool.

NuPrl

A tool supporting proof development in a ``New Proof/Program Refinement Logic'', which is a constructive type theory.

PRG

The Programming Research Group, at the University of Oxford.

set

A `small' collection.