pichardie05a

D. Pichardie, V. Rusu. Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method. Research Report Irisa, No 1766, November 2005.

Download [help]

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

We propose a practical method for defining and proving properties of general (i.e., not necessarily structural) recursive functions in proof assistants based on type theory. The idea is to define the graph of the intended function as an inductive relation, and to prove that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction principles for proving other arbitrary properties of the function. The approach has been experimented in the Coq proof assistant, but should work in like-minded proof asistants as well. It allows for functions with mutual recursive calls, nested recursive calls, and works also for the standard encoding of partial functions using total functions over a dependent type that restricts the original function's domain. We present simple examples and report on a larger case study (sets of integers represented as ordered lists of intervals) that we have conducted in the context of certified static analyses

Contact

Vlad Rusu http://www.irisa.fr/vertecs/Equipe/Rusu/vlad-rusu.html

BibTex Reference

@TechReport{pichardie05a,
   Author = {Pichardie, D. and Rusu, V.},
   Title = {Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method},
   Number = {1766},
   Institution = {Irisa},
   Month = {November},
   Year = {2005}
}

EndNote Reference [help]

Get EndNote Reference (.ref)