Winskel is (almost) Right: Towards a Mechanized Semantics Textbook
- 1 November 1998
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 10 (2), 171-186
- https://doi.org/10.1007/s001650050009
Abstract
We present a formalization of the first 100 pages of Winskel's textbook The Formal Semantics of Programming Languages in the theorem prover Isabelle/HOL: 2 operational, 2 denotational, 2 axiomatic semantics, a verification condition generator, and the necessary soundness, completeness and equivalence proofs, all for a simple imperative programming language.Keywords
This publication has 13 references indexed in Scilit:
- Type classes and overloading in higher-order logicPublished by Springer Science and Business Media LLC ,1997
- Possibly infinite sequences in theorem provers: A comparative studyPublished by Springer Science and Business Media LLC ,1997
- Traces of I/O-automata in Isabelle/HOLCFPublished by Springer Science and Business Media LLC ,1997
- Winskel is (almost) rightLecture Notes in Computer Science, 1996
- HOLCF: Higher order logic of computable functionsLecture Notes in Computer Science, 1995
- Reasoning with executable specificationsLecture Notes in Computer Science, 1995
- A mechanically verified verification condition generatorThe Computer Journal, 1995
- Report on the programming language HaskellACM SIGPLAN Notices, 1992
- Verification of Sequential and Concurrent ProgramsPublished by Springer Science and Business Media LLC ,1991
- Logic and ComputationPublished by Cambridge University Press (CUP) ,1987