coq-minic

Semantics of a subset of the C language. This contribution defines the denotational semantics of MiniC, a sub-set of the C language. This sub-set is sufficiently large to contain any program generated by lustre2C. The denotation function describing the semantics of a MiniC program actually provides an interpreter for the program.

opam install coq-minic.8.5.0
homepage
https://github.com/coq-contribs/minic
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/minic/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/minic/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-minic/coq-minic.8.5.0