Sciweavers

Share
JAR
2010

Partial and Nested Recursive Function Definitions in Higher-order Logic

8 years 6 months ago
Partial and Nested Recursive Function Definitions in Higher-order Logic
Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order logic (HOL) and provides appropriate proof rules for reasoning about them. Termination is modeled by an inductive domain predicate which follows the structure of the recursion. Since a partial induction rule is available immediately, partial correctness properties can be proved before termination is established. It turns out that this modularity also facilitates termination arguments for total functions, in particular for nested recursions. Our tool is implemented as a definitional package extending Isabelle/HOL. Various extensions provide convenience to the user: pattern matching, default values, tail recursion, mutual recursion and currying. Contents
Alexander Krauss
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Where JAR
Authors Alexander Krauss
Comments (0)
books