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.

• Type: Conference
• Year: 2000
• Where: TYPES
• Authors: Stefan Berghofer, Tobias Nipkow
• Keywords: Formal Methods, Inductive Definitions, Recursive Partial Functions, Theorem Prover Isabelle/hol, TYPES 2000