- Abstract:
-
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
- @InProceedings{EDI-INF-RR-0748,
- 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},
- }
|
