Coq is a formal proof management system which provides a pure functional language with nice dependent types together with an environment for writing machine-checked proofs.
- A Series on Strongly-Specified Funcions in Coq
- Using dependent types and the
Propsort, it becomes possible to specify functions whose arguments and results are constrained by properties. Using such a “strongly-specified” function requires to provide a proof that the supplied arguments satisfy the expected properties, and allows for soundly assuming the results are correct too. However, implementing dependently-typed functions can be challenging.
- A Series on Ltac
- Ltac is the “tactic language” of Coq. It is commonly advertised as the common approach to write proofs, which tends to bias how it is introduced to new Coq users (e.g., in Master courses). In this series, we present Ltac as the metaprogramming tool it is, since fundamentally it is an imperative language which allows for constructing Coq terms interactively and incrementally.
- Rewriting in Coq
rewritetactics are really useful, since they are not limited to the Coq built-in equality relation.
- A Study of Clight and its Semantics
- Clight is a “simplified” C AST used by CompCert, the certified C compiler. In this write-up, we prove a straighforward functional property of a small C function, as an exercise to discover the Clight semantics.
- Proving Algebraic Datatypes are “Algebraic”
- The set of types which can be defined in a language together with
*form an “algebraic structure” in the mathematical sense, hence the name. It means the definitions of
*have to satisfy properties such as commutativity or the existence of neutral elements.
- A Series on
coqffigenerates Coq FFI modules from compiled OCaml interface modules (
.cmi). In practice, it greatly reduces the hassle to together OCaml and Coq modules within the same codebase, especially when used together with the