Technical reports
A case study of co-induction in Isabelle HOL
Jacob Frost
August 1993, 27 pages
DOI: 10.48456/tr-308
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 higher-order logic of the generic theorem prover Isabelle.
Full text
PDF (0.2 MB)
PS (0.1 MB)
DVI (0.0 MB)
BibTeX record
@TechReport{UCAM-CL-TR-308, author = {Frost, Jacob}, title = {{A case study of co-induction in Isabelle HOL}}, year = 1993, month = aug, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-308.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-308}, number = {UCAM-CL-TR-308} }