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 the- ory inside type theory. The design choices underlying these representa- tions 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

https://hal.inria.fr/hal-00825074
Contributor : Assia Mahboubi <>
Submitted on : Wednesday, May 22, 2013 - 7:23:52 PM
Last modification on : Friday, February 6, 2015 - 12:34:41 PM
Long-term archiving on: Friday, August 23, 2013 - 4:16:34 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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

Share

Metrics

Record views

107

Files downloads

129