Department of Computer Science and Technology

Technical reports

A case study of co-induction in Isabelle HOL

Jacob Frost

August 1993, 27 pages

DOIhttps://doi.org/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}
}