Abstract | ||
---|---|---|
Abstract: We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational semantics, axiomatic semantics, and abstract interpretation. Descriptions as recursive functions are also provided whenever suitable, thus yielding a a verification condition generator and a static analyser that can be run inside the theorem prover for use in reflective proofs. Extraction of an inter- preter from the denotational semantics is also described. All different aspects are formally proved sound with respect to the natural semantics specification. Key-words: Coq, natural semantics, structural operational semantics, denotational se- |
Year | Venue | Keywords |
---|---|---|
2007 | Clinical Orthopaedics and Related Research | theorem proving,denotational semantics,axiomatic semantics,formal verification,programming language,theorem prover |
Field | DocType | Volume |
Denotational semantics of the Actor model,Formal semantics (linguistics),Operational semantics,Programming language,Normalisation by evaluation,Computational semantics,Denotational semantics,Action semantics,Algorithm,Mathematics,Well-founded semantics | Journal | abs/0707.0 |
Citations | PageRank | References |
4 | 0.48 | 17 |
Authors | ||
1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Yves Bertot | 1 | 442 | 40.82 |