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

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}
}