Title: Theory / Unimportant / CS / Programming / Coq / Certified Programming with Dependent Types

Name: Dependant type
Definition: A type system where some complex computational expression may be part of the type
Page: 9
Chapter: 1
Section: 2.1

Name: A proof assistant satistfying the de Bruijn criterion
Definition: A proof assistant which produce proof terms in small kernel language
Page: 9
Chapter: 1
Section: 2.1
Intuition: There is very few to trust, everything else is based on top of the kernel

Name: ltac
Definition: Coq language for decision procedure
Page: 9
Chapter: 1
Section: 2.4

Question: Logical properties of Calculus of Inductive Construction
Answer: Relative consistency with ZF
Page: 19
Chapter: 2
Answer2: Strong normalization

Name: Vernacular
Definition: Gallina
Page: 19
Chapter: 2
Context: Coq
Definition2: ltac
Conjdef: It contains in particular
DefType: The language of Coq.

Name: Gallina
Definition: The extension of CIC used to express various term in coq
Page: 19
Chapter: 2
Context: Coq

Name: Interactive proof-editing mode
Definition: coq mode used to interactively write proof
Page: 22
Chapter: 2
Section: 1.4
Context: coq

Instruction: SearchRewrite pattern.
Page: 25
Effect: Print rewrite rules that follows pattern
Language: coq
Chapter: 2
Section: 1.4

Name: Indexed type family
Definition: A type definition taking parameters
Page: 30
Chapter: 2
Example: Inductive tbinop : type → type → type → Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq : ∀ t, tbinop t t Bool
| TLt : tbinop Nat Nat Bool.

Name: Generalized algebraic datatypes
Page: 31
Chapter: 2
Abbreviation: GADTs

Name: Program extraction
Definition: The process of transforming a vernacular into executable code
Page: 37
Chapter: 2

Question: Difference between true/false and True/False
Answer: The metatheory garantee that all bool evaluates to true/false. On the otherhand not all propositions can evaluate to True/False, some are undecidable
Page: 41
Chapter: 3
Section: 1
Context: coq

Instruction: Scheme foo_1 := Induction for t_1 Sort Prop
...
with foo_n := Induction for t_n Sort Prop
Page: 52
Meaning: induction rules that takes a property P_i applied to each type t_i. If for each foo element of type t_i where its arguments of type t_j satisfies P_j, then P_i holds, then P_i holds for all elements of type t_i
Chapter: 3
Section: 5
Identifier: foo_i

Instruction: apply T
Page: 53
Effect: replace the current goal by the hypothesis of T
Chapter: 3
Section: 5
Variables: T a theorem
G the current goal
Assuming: the conclusion of T matches G
Intuition: We want to prove the conclusion of T, for so we must prove its hypothesis

Name: A reflexive type
Definition: A type T with a constructor taking as argument a function returning a value of type T
Page: 54
Chapter: 3
Section: 6
Example: Inductive formula : Set :=
  | Forall : (nat -> formula) -> formula

Name: high order abstract syntax
Page: 55
Chapter: 3
Section: 6
Abbreviation: HOAS

Question: What is the restriction on inductive type in Coq
Answer: When defining a type T, all constructors only have positive uses of T
Page: 56
Chapter: 3
Section: 6
Context: Coq

Name: A type occuring positively in t_1 -> ... -> t_n -> t
Definition: The type t
Page: 56
Chapter: 3
Section: 6
Variables: t_1 -> ... -> t_n -> t
Context: Coq

Name: A type occuring negatively in t_1 -> ... -> t_n -> t
Definition: A type t_i
Page: 56
Chapter: 3
Section: 6
Variables: t_1 -> ... -> t_n -> t
Context: Coq