Generic Proof Tools and Finite Group Theory

摘要: This thesis presents advances in the use of Canonical Structures, a programming language construct Coq proof assistant equivalent to notion type classes. It provides new model for developping hierarchies mathematical structures using dependent records, and, as an illustration, reformulates common formal correctness RSA cryptosystem, providing facilities algebraic reasoning along with formalization theory necessary notions (including cyclic groups, automorphism group isomorphisms). We provide extension Structure inference mechanism phantom types, and apply it treating partial functions. Next, we consider generic treatment several forms subgroup definitions occurring Feit-Thompson theorem, large library fomalized algebra developed Mathematical Components team at MSR-INRIA joint laboratory. show that unified those 16 subgroups allows us shorten menial proofs obtain more composable definitions. formalize correspondence between study functorials, some useful group-theoretic properties represented class groups verifying them. conclude exploring possibilities analyzing functoriality by inspecting their type, suggest path towards obtaining instances parametricity result Coq.