A modular formalisation of finite group theory

Georges Gonthier; Assia Mahboubi; Laurence Rideau; Enrico Tassi; Laurent Théry

doi:10.1007/978-3-540-74591-4_8

A modular formalisation of finite group theory

Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

In this paper, we present a formalisation of elementary group theory done in COQ. This work is the first milestone of a long-term effort to formalise the Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way. © Springer-Verlag Berlin Heidelberg 2007.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings
Publisher	Springer Verlag
Pages	86-101
ISBN (Print)	9783540745907
DOIs	https://doi.org/10.1007/978-3-540-74591-4_8
Publication status	Published - 2007
Externally published	Yes
Event	20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 - , Germany Duration: 10 Sept 2007 → 13 Sept 2007

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007
Country/Territory	Germany
Period	10/09/07 → 13/09/07

Access to Document

10.1007/978-3-540-74591-4_8

Persistent URL (handle)

Persistent link

Cite this

Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., & Théry, L. (2007). A modular formalisation of finite group theory. In Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings (pp. 86-101). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Springer Verlag. https://doi.org/10.1007/978-3-540-74591-4_8

Gonthier, Georges ; Mahboubi, Assia ; Rideau, Laurence et al. / A modular formalisation of finite group theory. Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, 2007. pp. 86-101 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{66894e1dce0e4897bf5a469e4cd82a70,

title = "A modular formalisation of finite group theory",

abstract = "In this paper, we present a formalisation of elementary group theory done in COQ. This work is the first milestone of a long-term effort to formalise the Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way. {\textcopyright} Springer-Verlag Berlin Heidelberg 2007.",

author = "Georges Gonthier and Assia Mahboubi and Laurence Rideau and Enrico Tassi and Laurent Th{\'e}ry",

year = "2007",

doi = "10.1007/978-3-540-74591-4_8",

language = "English",

isbn = "9783540745907",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "86--101",

booktitle = "Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings",

note = "20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 ; Conference date: 10-09-2007 Through 13-09-2007",

}

Gonthier, G, Mahboubi, A, Rideau, L, Tassi, E & Théry, L 2007, A modular formalisation of finite group theory. in Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Verlag, pp. 86-101, 20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007, Germany, 10/09/07. https://doi.org/10.1007/978-3-540-74591-4_8

A modular formalisation of finite group theory. / Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence et al.
Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, 2007. p. 86-101 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A modular formalisation of finite group theory

AU - Gonthier, Georges

AU - Mahboubi, Assia

AU - Rideau, Laurence

AU - Tassi, Enrico

AU - Théry, Laurent

PY - 2007

Y1 - 2007

N2 - In this paper, we present a formalisation of elementary group theory done in COQ. This work is the first milestone of a long-term effort to formalise the Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way. © Springer-Verlag Berlin Heidelberg 2007.

AB - In this paper, we present a formalisation of elementary group theory done in COQ. This work is the first milestone of a long-term effort to formalise the Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way. © Springer-Verlag Berlin Heidelberg 2007.

UR - http://www.scopus.com/inward/record.url?scp=38049031798&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-74591-4_8

DO - 10.1007/978-3-540-74591-4_8

M3 - Conference contribution

SN - 9783540745907

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 86

EP - 101

BT - Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings

PB - Springer Verlag

T2 - 20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007

Y2 - 10 September 2007 through 13 September 2007

ER -

Gonthier G, Mahboubi A, Rideau L, Tassi E, Théry L. A modular formalisation of finite group theory. In Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag. 2007. p. 86-101. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-74591-4_8

A modular formalisation of finite group theory

Abstract

Publication series

Conference

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this