The expressiveness of our formal system is sufficient we believe to define the denotational semantics of application development languages. By providing a logically secure framework within which specialised type theories with matching derived inference rules may be established, we hope to enable a close fit between application languages and specification languages. This may enable a development methodology in which specifications are evolved into implementations by stages which are supported by automatic verification.

up home © RBJ dated 86/7/15 HTML 96/6/6 edited 96/6/15