Executing Higher Order Logic

13 years 9 months ago
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.
Stefan Berghofer, Tobias Nipkow
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Authors Stefan Berghofer, Tobias Nipkow
Comments (0)