Executing Higher Order Logic
We report on the design of a prototyping component for the theorem prover
Isabelle/HOL. Specifications consisting of datatypes, recursive functions
and inductive definitions are compiled into a functional program. Functions
and inductively defined relations can be mixed. Inductive definitions must be
such that they can be executed in Prolog style but requiring only matching
rather than unification. This restriction is enforced by a mode
analysis. Tail recursive partial functions can be defined and executed with
the help of a while-combinator.
pdf
BibTeX:
@inproceedings{BerghoferN-TYPES00,
author={Stefan Berghofer and Tobias Nipkow},
title={Executing Higher Order Logic},
booktitle={Types for Proofs and Programs (TYPES 2000)},
editor={P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
year=2002,publisher=Springer,series=LNCS,volume=2277,pages="24--40"}