Recent Posts
-
Basic Tactics and Underlying LogicThis post explain basic and common tactics in Coq and their underlying logic.
-
Templates in CPPTemplates, Concepts and Polymorphism
-
Polymorphism and Higher-order Function in Coqabstracting and reusing functions
-
Runtime Polymorphism in CPPPure Virtual Classes as Interfaces, Runtime Polymorphism by Composition
-
Reasoning Proofs with Basic Data StructuresPair, List, Map, Options
-
Induction, Sub-theorems and Informal Proof [Coq]Study Notes of software validation