MODELS AND METAMODELS FOR SOFTWARE VERIFICATION AND VALIDATION
Logical frameworks High order recursive types Proof assistants 1 Proof assistants 2 Examples General computational paradigm Basic encoding principles 1 Basic encoding principles 2 Higher order abstract syntax 1 Higher order abstract syntax 2 Higher order natural deduction Further features The Coq proof assistant 1 The Coq proof assistant 2 The calculus of inductive constructions 1 The calculus of inductive constructions 2 CIC: some rules Coq languages: Gallina and the vernacular Induction Principles and Recursion (Co)inductively defined predicates (relations) Representing binding operators 1 Representing binding operators 2 Representing binding operators 3 Using Coq as a LF for specifing first order logic 1 Using Coq as a LF for specifing first order logic 2 HOAS and inductive types HOAS and inductive types: delegating only a-equivalence 1 HOAS and inductive types: delegating only a-equivalence 2 HOAS and inductive types: exotic terms HOAS and inductive types: ruling out exotic terms HOAS and inductive types: avoiding exotic terms HOAS and inductive types: a theory of contexts 1 HOAS and inductive types: a theory of contexts 2 Initial semantics Final semantics Dualities Final semantics as a metamodels 1 Final semantics as a metamodels 2 Scope of final semantics
