Hostname: page-component-7c8c6479df-hgkh8 Total loading time: 0 Render date: 2024-03-27T13:15:20.858Z Has data issue: false hasContentIssue false

Implementing theorem provers in a purely functional style

Published online by Cambridge University Press:  01 March 1999

KEITH HANNA
Affiliation:
Computing Laboratory, University of Kent, UK (e-mail: fkh@ukc.ac.uk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Copyright
© 1999 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.