Technical reports
A case study of co-induction in Isabelle
Jacob Frost
February 1995, 48 pages
DOI: 10.48456/tr-359
Abstract
The consistency of the dynamic and static semantics for a small functional programming language was informally proved by R. Milner and M. Tofte. The notions of co-inductive definitions and the associated principle of co-induction played a pivotal role in the proof. With emphasis on co-induction, the work presented here deals with the formalisation of this result in the generic theorem prover Isabelle.
Full text
PDF (0.2 MB)
PS (0.1 MB)
DVI (0.1 MB)
BibTeX record
@TechReport{UCAM-CL-TR-359, author = {Frost, Jacob}, title = {{A case study of co-induction in Isabelle}}, year = 1995, month = feb, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-359.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-359}, number = {UCAM-CL-TR-359} }