package coq-semantics

  1. Overview
  2. No Docs
A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation

Install

Dune Dependency

Authors

Maintainers

Sources

v8.9.0.tar.gz
md5=d141ec48c51619b2672f12d6c740d87a

Description

This is a survey of programming language semantics styles for a miniature example of a programming language, with their encoding in Coq, the proofs of equivalence of different styles, and the proof of soundess of tools obtained from axiomatic semantics or abstract interpretation. The tools can be run inside Coq, thus making them available for proof by reflection, and the code can also be extracted and connected to a yacc-based parser, thanks to the use of a functor parameterized by a module type of strings. A hand-written parser is also provided in Coq, but there are no proofs associated.

Dependencies (3)

  1. coq >= "8.9" & < "8.10~"
  2. ocamlbuild build
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None