%0 Journal Article %1 nipkow_98_winskel %A Nipkow, Tobias %D 1998 %J Formal Aspects of Computing %K 1998 semantics mechanized operational denotational %N 2 %P 171--186 %R 10.1007/s001650050009 %T Winskel is (almost) Right: Towards a Mechanized Semantics Textbook %U http://dx.doi.org/10.1007/s001650050009 %V 10 %X 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.

@article{nipkow_98_winskel, abstract = {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.}, added-at = {2009-02-12T11:19:25.000+0100}, author = {Nipkow, Tobias}, biburl = {https://www.bibsonomy.org/bibtex/2c0f47bee8dca912adcdec8e465f961f7/leonardo}, citeulike-article-id = {3788238}, doi = {10.1007/s001650050009}, interhash = {1eec9aca038cdc1e4b4f7d2a2f983d42}, intrahash = {c0f47bee8dca912adcdec8e465f961f7}, journal = {Formal Aspects of Computing}, keywords = {1998 semantics mechanized operational denotational}, month = {November}, number = 2, pages = {171--186}, posted-at = {2008-12-15 00:26:58}, priority = {4}, timestamp = {2009-02-12T11:19:25.000+0100}, title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, url = {http://dx.doi.org/10.1007/s001650050009}, volume = 10, year = 1998 }