Executing Higher Order Logic

Stefan Berghofer and Tobias Nipkow

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.

ps pdf


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},