[Prev][Next][Index][Thread]
Co-induction by ftp
The following paper, about co-induction in Isabelle HOL, is available by
anonymous ftp from the University of Cambridge. Instructions:
* Connect to host ftp.cl.cam.ac.uk
* Use login id "ftp" with your internet address as password
* put ftp in BINARY MODE ("binary")
* go to directory ml (by typing "cd ml")
* "get" the files coind.dvi.Z and coind-fig.ps.Z from that directory.
Comments welcome! Also please let me know if you encounter difficulties.
Larry Paulson
Co-induction and Co-recursion in Higher-order Logic
Lawrence C Paulson
Abstract
A theory of recursive and corecursive definitions has been developed in
higher-order logic (HOL) and mechanised using Isabelle. Least fixedpoints
express inductive data types such as strict lists; greatest fixedpoints
express co-inductive data types, such as lazy lists. Well-founded
recursion expresses recursive functions over inductive data types;
co-recursion expresses functions that yield elements of co-inductive data
types. The theory rests on a traditional formalization of infinite trees.
The theory is intended for use in specification and verification. It
supports reasoning about a wide range of computable functions, but it does
not formalize their operational semantics and can express noncomputable
functions also. The theory is demonstrated using lists and lazy lists as
examples. The emphasis is on using co-recursion to define lazy list
functions, and on using co-induction to reason about them.