Sciweavers

Share
FUIN
2010

Automation for Dependently Typed Functional Programming

9 years 7 months ago
Automation for Dependently Typed Functional Programming
Abstract. Writing dependently typed functional programs that capture non-trivial program properties, such as those involving membership, ordering and non-linear arithmetic, is difficult in current system due to lack of proof automation. We identify and discuss proof patterns that occur when programming with dependent types and detail how the automation of such patterns allow us to work more comfortably with types, particularly subset types, that capture such program properties. We describe the application of rippling, both for inductive and non-inductive proofs, and generalisation in discharging proof obligations that arise when programming with dependent types. We then discuss an implementation of our ideas in Coq with examples of practical programs that capture useful properties. We demonstrate that our proof automation is generic in that it can provide support for working with theorems involving user-defined inductive data types and functions.
Sean Wilson, Jacques D. Fleuriot, Alan Smaill
Added 02 Mar 2011
Updated 02 Mar 2011
Type Journal
Year 2010
Where FUIN
Authors Sean Wilson, Jacques D. Fleuriot, Alan Smaill
Comments (0)
books