Computer Science – Programming Languages
Scientific paper
2010-10-27
Logics and languages for reliability and security, J. Esparza and B. Spanfelner and O. Grumberg (Ed.) (2010) 195-224
Computer Science
Programming Languages
Scientific paper
10.3233/978-1-60750-100-8-195
The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and over generic program transformations, as typically found in compilers. The topics covered include: operational semantics (small-step, big-step, definitional interpreters); a simple form of denotational semantics; axiomatic semantics and Hoare logic; generation of verification conditions, with application to program proof; compilation to virtual machine code and its proof of correctness; an example of an optimizing program transformation (dead code elimination) and its proof of correctness.
No associations
LandOfFree
Mechanized semantics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Mechanized semantics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Mechanized semantics will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-484697