TY - GEN
T1 - Winskel is (almost) right
T2 - 16th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 1996
AU - Nipkow, Tobias
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1996.
PY - 1996
Y1 - 1996
N2 - We present a formalization of the first 100 pages of Winskel's The Formal Semantics of Programming Languages in the theorem prover Isabelle/HOL: 2 operational, 2 denotational, 1 axiomatic semantics, a verification condition generator, and the necessary soundness, completeness and equivalence proofs, all for a simple imperative language.
AB - We present a formalization of the first 100 pages of Winskel's The Formal Semantics of Programming Languages in the theorem prover Isabelle/HOL: 2 operational, 2 denotational, 1 axiomatic semantics, a verification condition generator, and the necessary soundness, completeness and equivalence proofs, all for a simple imperative language.
UR - http://www.scopus.com/inward/record.url?scp=84947922868&partnerID=8YFLogxK
U2 - 10.1007/3-540-62034-6_48
DO - 10.1007/3-540-62034-6_48
M3 - Conference contribution
AN - SCOPUS:84947922868
SN - 3540620346
SN - 9783540620341
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 180
EP - 192
BT - Foundations of Software Technology and Theoretical Computer Science - 16th Conference 1996, Proceedings
A2 - Chandru, Vijay
A2 - Vinay, V.
PB - Springer Verlag
Y2 - 18 December 1996 through 20 December 1996
ER -