Computer Laboratory

Technical reports

A case study of co-induction in Isabelle

Jacob Frost

February 1995, 48 pages

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 = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-359.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-359}
}