Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

15

CORR
2010
Springer

favoriteEmaildiscussreport

147views Education» more CORR 2010»

Mechanized semantics

13 years 4 months ago

Mechanized semantics

Download gallium.inria.fr

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.

Xavier Leroy

Real-time Traffic

Coq Proof | CORR 2010 | Education | Program Transformation | Semantics |

claim paper

Related Content

» Named Graphs as a Mechanism for Reasoning About Provenance

» Argumentation Mechanism Design for Preferred Semantics

» A mechanized semantics for C object construction and destruction with applications to reso...

» An Autonomic Service Discovery Mechanism to Support Pervasive Device Accessing Semantic Gr...

» A Caching Mechanism for Semantic Web Service Discovery

» Parametric higherorder abstract syntax for mechanized semantics

» Logic as a Power Tool to Model Negotiation Mechanisms in the Semantic Web Era

» A Semantic Web based Identification Mechanism for Databases

» Cluster Mechanisms in a Selforganizing Distributed Semantic Store

Post Info
More Details (n/a)

Added	09 Dec 2010
Updated	09 Dec 2010
Type	Journal
Year	2010
Where	CORR
Authors	Xavier Leroy

Comments (0)