The Rooster and the Butterflies

Abstract : This paper describes a machine-checked proof of the Jordan- Hölder theorem for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the Odd Order Theorem with the Coq system.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-00825074
Contributor : Assia Mahboubi <>
Submitted on : Monday, July 15, 2013 - 9:31:51 PM
Last modification on : Thursday, February 9, 2017 - 3:48:06 PM
Long-term archiving on : Wednesday, April 5, 2017 - 12:20:18 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Assia Mahboubi. The Rooster and the Butterflies. CICM 2013 - Conference on Intelligent Computer Mathematics - 2013, Jul 2013, Bath, United Kingdom. pp.1-18, ⟨10.1007/978-3-642-39320-4_1⟩. ⟨hal-00825074v3⟩

Share

Metrics

Record views

562

Files downloads

437