As I said, the Coq proof assistant is essentially a proof development environment for the higher order constructive type theory consisting of the calculus of inductive constructions. And so, it is the implementation of the logical framework. What you do, you write specifications, you develop interactive proofs, you check existing proofs in batch, you reuse previously defined proofs and specifications, you abstract programs from proofs according to the paradigm that was outlined in the previous lecture.

---