Sciweavers

ENTCS
2006
169views more  ENTCS 2006»
13 years 11 months ago
Constructing Induction Rules for Deductive Synthesis Proofs
We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of ...
Alan Bundy, Lucas Dixon, Jeremy Gow, Jacques D. Fl...
CSL
2010
Springer
14 years 16 days ago
Fibrational Induction Rules for Initial Algebras
This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our res...
Neil Ghani, Patricia Johann, Clément Fumex
LPAR
1999
Springer
14 years 3 months ago
Extensions to the Estimation Calculus
Abstract. Walther’s estimation calculus was designed to prove the termination of functional programs, and can also be used to solve the similar problem of proving the well-founde...
Jeremy Gow, Alan Bundy, Ian Green