Winskel is (almost) Right: Towards a Mechanized Semantics Textbook

Tobias Nipkow

doi:10.1007/s001650050009

Winskel is (almost) Right: Towards a Mechanized Semantics Textbook

Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Research output: Contribution to journal › Article › peer-review

56 Scopus citations

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	https://doi.org/10.1007/s001650050009
State	Published - 1998

Keywords

HOL
Higher-order logic
Isabelle
Programming language
Semantics
Theorem proving

Access to Document

10.1007/s001650050009

Cite this

@article{ac4d601511ac418c9b8a93e89c8f31ab,

title = "Winskel is (almost) Right: Towards a Mechanized Semantics Textbook",

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 = "HOL, Higher-order logic, Isabelle, Programming language, Semantics, Theorem proving",

author = "Tobias Nipkow",

year = "1998",

doi = "10.1007/s001650050009",

language = "English",

volume = "10",

pages = "171--186",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery (ACM)",

number = "2",

}

TY - JOUR

T1 - Winskel is (almost) Right

T2 - Towards a Mechanized Semantics Textbook

AU - Nipkow, Tobias

PY - 1998

Y1 - 1998

N2 - 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.

AB - 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.

KW - HOL

KW - Higher-order logic

KW - Isabelle

KW - Programming language

KW - Semantics

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=0013135170&partnerID=8YFLogxK

U2 - 10.1007/s001650050009

DO - 10.1007/s001650050009

M3 - Article

AN - SCOPUS:0013135170

SN - 0934-5043

VL - 10

SP - 171

EP - 186

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 2

ER -

Winskel is (almost) Right: Towards a Mechanized Semantics Textbook

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this