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.
| Original language | English |
|---|---|
| Pages (from-to) | 171-186 |
| Number of pages | 16 |
| Journal | Formal Aspects of Computing |
| Volume | 10 |
| Issue number | 2 |
| DOIs | |
| State | Published - 1998 |
Keywords
- HOL
- Higher-order logic
- Isabelle
- Programming language
- Semantics
- Theorem proving
Fingerprint
Dive into the research topics of 'Winskel is (almost) Right: Towards a Mechanized Semantics Textbook'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver