This paper discusses the principles of implementing an LCF-style proof assistant using a purely
functional metalanguage. Two approaches are described; in both, signatures are treated as
ordinary values, rather than as mutable components within an abstract datatype. The first
approach treats the object logic as a partial algebra and represents it as a partial datatype, that
is, a datatype in which the domains of the constructors are restricted by predicate functions.
This results in a compact, executable specification of the logic. The second approach uses
an abstract type to allow an efficient representation of the logic, whilst keeping the same
interface. A case study describes how these principles were put into practice in implementing
a fairly complex dependently-sorted logic.
An executable specification of an argumentation protocol
