Coq
 Coq is Normal
 Canonical Structures
 Kernel
 Ocaml
 Plugins
 Iris
 SSReflect
 Stdlibs
 Prolog
 Compcert
 Examples
 Misc
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 normalish functional programming language.
See my Coq in Y Minutes tutorial
Cody’s intro to coq https://github.com/codyroux/broadcoqtutorial
Inductive weekday :=
 monday
 tuesday.
Interesting commands
Drop
vernacular  srops you into an ocaml toplevel Register making names accessible to ocaml
 [Primitive]  register an ocaml primitive
Show
gives infromation during proof.Show Proof
shows intermediate stuff.Search
. Very important. Lots of features.
Inductive Types
Inductive types are prolog
Eliminators and pattern matching
What should be primitive anyway?
Coinductive Types
Reflection
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
Canonical Structures
https://coq.inria.fr/refman/language/extensions/canonical.html
canonical structures for the working coq user Register in a database how to go from a projection of a structure to the structure itself. Kind of sort of we are declaring that projectors are injective.
https://okmij.org/ftp/ML/canonical.html Oleg discussing aspects of the system.
Kernel
VM
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 https://cstheory.stackexchange.com/questions/18777/iscompilerfordependenttypemuchharderthananintepreter leroy gergoire paper bytecode interpreter full reduction at full throttle
Ocaml
There are plugin tutorials Coq is available as a library. coqcore. Note the Ocam API documentation https://coq.github.io/doc/
 coqsimpleio
 coqffi generates ffi boilerplate for ocaml functions
Plugins
.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
Iris
Higher order separation logic. Kind of modelling concurrent ML in Coq I think?
SSReflect
SSReflect emphasizes proof by reflection. It is a really succinct inscrutable looking syntax.
Stdlibs
Prolog
Compcert
https://github.com/AbsInt/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
Coq hackthan 2022
https://github.com/coq/coq/tree/master/dev/doc https://github.com/coq/coq/wiki/DevelSetup 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
 names.ml
 univ.ml
 sorts.ml
 constr.ml  internal syntax of terms. “constructions”

native*.ml stuff related to native compilation to ocaml for normalization
 testuite
 ide  coq ide
 boot
types
 constr
 unsafe_judgement
 evar_map

glob_constr
You can build coq using dune make f Makefile.dune
https://github.com/ejgallego/coq/tree/simple_compiler
stm
parse resolution of names interpret type inferrance
compiler/scoq.c vernac com* are implementationso f that vernac vernacexpr.ml 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?
evar_map
gramlib?
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
https://github.com/ejgallego/coqserapi/blob/v8.13/FAQ.md#howmanyastsdoescoqhave
dune
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
 scan all stanzas
 build virtual view of file system
 setup rule
 build a target
(coq.theory
)
 we detect dune file with (coq.theory
 extract generated files
 setup rules, informrm the build enginer about what net targets are in scope
Examples
Compute 1 + 1.
Equality eliminator is rewriting.
Misc
https://github.com/stepchowfun/proofs/blob/main/proofs/Tutorial/Lesson5_Consistency.v in particular
https://github.com/dwarfmaster/commutativediagrams tactic for categroy proofs
 coqceres 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 acceptDefinition foo (a : A) (b : B) (c : C) : F := f.
It sort of reorders the pieces and make you give a name to the whole judgementfoo
. That’s an interesting way of looking at it anyway. Of course the more usual way is thatfoo
is a function definition.
Leroy and Appell caonical binary trees
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
ringer pluin tutorial talia ringer thesis really good explanations
Modular preprocessing for automated reasoning in dependent type theory processing for smtcoq The proPER meaning of “proper”
metamatix verified implementatyion of metamath checker https://github.com/acorrenson/WiSE  verified bug finding https://github.com/acorrenson/minilog  verified implementation of mini prolog
defaultt  default logic
https://github.com/acorrenson/SATurne