@inproceedings{d4defcba59954a64a8011f2c5d4e6140,
title = "Reasoning About CBV Functional Programs in Isabelle/HOL",
abstract = "We consider the old problem of proving that a computer program meets some specification. By proving, we mean machine checked proof in some formal logic. The programming language we choose to work with is a call by value functional language, essentially the functional core of Standard ML (SML). In future work we hope to add exceptions, then references and I/O to the language.",
author = "John Longley and Randy Pollack",
year = "2004",
doi = "10.1007/978-3-540-30142-4_15",
language = "English",
isbn = "978-3-540-23017-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "201--216",
editor = "Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan",
booktitle = "Theorem Proving in Higher Order Logics",
address = "United Kingdom",
}