Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Reasoning about CBV functional programs in Isabelle/HOL
Authors: John Longley ; Robert Pollack
Date:Sep 2004
Publication Title:Proceedings of TPHOLs 2004 (International Conference on Theorem Proving in Higher Order Logics)
Publication Type:Conference Paper Publication Status:Published
Volume No:3223 Page Nos:201-216
While the full SML language has a formal definition by a big-step operational semantics, this does not support convenient reasoning about programs. We develop a high level program logic that is useful for reasoning about features such as recursive functions and datatypes. The logic makes use of purely operational concepts, such as observational equivalence of program fragments. Thus the logic will be intelligible to programmers with no knowledge of the semantic underpinnings. On the other hand, the logic is justified by denotational models. This is achieved by using models that enjoy a tight fit with the programming language via the concept of logical full abstraction.
Links To Paper
No links available
Bibtex format
author = { John Longley and Robert Pollack },
title = {Reasoning about CBV functional programs in Isabelle/HOL},
book title = {Proceedings of TPHOLs 2004 (International Conference on Theorem Proving in Higher Order Logics)},
publisher = {Springer},
year = 2004,
month = {Sep},
volume = {3223},
pages = {201-216},
doi = {10.1007/b100400},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh