Department of Computer Science and Technology

Technical reports

A case study of co-induction in Isabelle

Jacob Frost

February 1995, 48 pages

DOI: 10.48456/tr-359


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

  author =	 {Frost, Jacob},
  title = 	 {{A case study of co-induction in Isabelle}},
  year = 	 1995,
  month = 	 feb,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-359},
  number = 	 {UCAM-CL-TR-359}