See also:

  • Type theory
  • Proof theory
  • HOTT
  • Higher order unification

Coq is Normal

Coq has all sorts of crazy stuff in it, but the core of it can be used as a normal-ish functional programming language.

See my Coq in Y Minutes tutorial

Interesting commands

  • Drop vernacular - srops you into an ocaml toplevel
  • Register
  • [Primitive] - register an ocaml primitive

Inductive Types

Inductive types are prolog

Eliminators and pattern matching

What should be primitive anyway?

Coindcutive Types


You can use domain specific ADTs to describe a class of problems. You can use coq as an ordinary programming language

What are Proofs

match annotations

The as annotation is a realtive of the ocaml as annotation. It is a binding form. Likewise for the in annotation. This is a pattern matching annotation that binds pattern variables. The scope of the bindings is only over the return clause of the match. These annotations bring the match closer or exactly equivalent to the “recursor” formulation of pattern matching. This is a higher order function that you give a function specify what to do in each case. In the dependent context, you also give it a return type function.

In any sense does this



There is a coq vm with a bytecode. The instructions are defined here

Is this bytecode interpreter described anywhere?

Cody suggests Benjamin Gregoire

Sometimes is feels like cody knows a lot leroy gergoire paper bytecode interpreter full reduction at full throttle


There are plugin tutorials Coq is available as a library. coq-core. Note the Ocam API documentation


plugin tutorials

.mlg files huh? Those are weird I don’t know that any of this is documented except in these tutorials

coqpp is the tool that turns .mlg into .ml files


  • coq-ceres coq sexp stuff
  • QED does something serious.
  • Surface coq is desugared
  • match annnotations are
  • Note that the judgement a : A, b : B, c : C |- f : F is sort of getting Coq to accept Definition foo (a : A) (b : B) (c : C) : F := f. It sort of reorders the pieces and make you give a name to the whole judgement foo. That’s an interesting way of looking at it anyway. Of course the more usual way is that foo is a function definition.

Leroy and Appell caonical binary trees


Higher order separation logic. Kind of modelling concurrent ML in Coq I think?

Compcert manual The long form compcert paper seems the most useful

An interpreter of C. It stops if it hits undefined behavior? That’s cool. This seems really useful even for a non verified version

C -> Clight -> C#minor -> Cminor -> CminoSel -> RTL -> LTL -> Linear 0> Mach

Individual folders for each architecture. Interesting.

  • backend

autosubst VCFloat gappa flocq mathematical components coq platform

Verified software Toolchain higher order separation logic for C certigraph graph manipulation programs certigc verified garbage collector

Axioms to consider enabling

ringer pluin tutorial

Coq hackthan 2022 coq devel setup

  • dev helpful information and scripts
  • kernel
  • interp
  • vernac - all sorts of files implementing vernacular commands fixpoint, indcutive, define search etc
  • tactics - ocaml code implementing some built in tactics like auto, autorewrite,
  • pretyping? Is this elaboration from surface syntax to kernel.
  • plugins - some native plugins are implemented. Extraction, btauto. Possibly a good place to look if you want to implement your own plguin. ssr. ring. micromega, ltac, ltac2
  • kernel. I’ll try to list these in a dependency order
    • - internal syntax of terms. “constructions”
    • native*.ml stuff related to native compilation to ocaml for normalization
  • testuite
  • ide - coq ide
  • boot


  • constr
  • unsafe_judgement
  • evar_map
  • glob_constr

You can build coq using dune make -f Makefile.dune


parse resolution of names interpret type inferrance

compiler/scoq.c vernac com* are implementationso f that vernac vernac as VerancExtend constructor is where extension points hook in

using serapi to probe coq ast camlp5 mlg files. you can find them in _build vernacentires - interpeter out of vernac vernacextend.mli a typed dsl for vernac vernax_interp vernac_state declare.mli

Wehen you do a lemma Proof_info interp/Constrintern first step of elbation

interp/constrr_expr is surface syntax of coq terms. pretyping/glob_contr globalized /internalized term name resolution applied pretyping.mli type inferrence pretyping/understand_tcc is an important entry point?



pretypinggggggggg evarconv.mli what is this?

libraries coq_checklib bool clib config coqpp top printer engine 0 actual proof engine gramlib interp kernel lib library parsing parsing pretypng printing parsing proofs legacy sysinti tactics tactics vernac

engine is 2 compoenents in one. pconstr e


make problmatic

couple of pointers

  • build systems a la carte
  • podcast about build systems by andrey

language agnostic language secpfic rules in dunesrc dep.mli memo.mli - memo is important huh. Build monad src/dune_rules

  1. scan all stanzas
  2. build virtual view of file system
  3. setup rule
  4. build a target



  1. we detect dune file with (coq.theory
  2. extract generated files
  3. setup rules, informrm the build enginer about what net targets are in scope


Compute 1 + 1.

Equality eliminator is rewriting.


talia ringer thesis really good explanations

Modular pre-processing for automated reasoning in dependent type theory processing for smtcoq The pro-PER meaning of “proper”