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