×

zbMATH — the first resource for mathematics

McLaughlin, Sean

Compute Distance To:
Author ID: mclaughlin.sean Recent zbMATH articles by "McLaughlin, Sean"
Published as: McLaughlin, Sean; Mclaughlin, Sean
Homepage: http://www.cs.cmu.edu/~seanmcl/papers/index.html
External Links: dblp
Documents Indexed: 9 Publications since 2005

Publications by Year

Citations contained in zbMATH

9 Publications have been cited 66 times in 61 Documents Cited by Year
A revision of the proof of the Kepler conjecture. Zbl 1195.52004
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland
14
2010
A proof-producing decision procedure for real arithmetic. Zbl 1135.03329
McLaughlin, Sean; Harrison, John
12
2005
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland
11
2017
Cooperating theorem provers: a case study combining HOL-Light and CVC Lite. Zbl 1272.68362
Mclaughlin, Sean; Barrett, Clark; Ge, Yeting
10
2006
An interpretation of Isabelle/HOL in HOL Light. Zbl 1222.68370
McLaughlin, Sean
6
2006
The dodecahedral conjecture. Zbl 1207.52017
Hales, Thomas C.; McLaughlin, Sean
5
2010
Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. Zbl 1182.68212
McLaughlin, Sean; Pfenning, Frank
5
2008
Efficient intuitionistic theorem proving with the polarized inverse method. Zbl 1250.03019
McLaughlin, Sean; Pfenning, Frank
2
2009
Tool building requirements for an API to first-order solvers. Zbl 1272.68358
Grundy, Jim; Melham, Tom; Krstić, Sava; McLaughlin, Sean
1
2006
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland
11
2017
A revision of the proof of the Kepler conjecture. Zbl 1195.52004
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland
14
2010
The dodecahedral conjecture. Zbl 1207.52017
Hales, Thomas C.; McLaughlin, Sean
5
2010
Efficient intuitionistic theorem proving with the polarized inverse method. Zbl 1250.03019
McLaughlin, Sean; Pfenning, Frank
2
2009
Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. Zbl 1182.68212
McLaughlin, Sean; Pfenning, Frank
5
2008
Cooperating theorem provers: a case study combining HOL-Light and CVC Lite. Zbl 1272.68362
Mclaughlin, Sean; Barrett, Clark; Ge, Yeting
10
2006
An interpretation of Isabelle/HOL in HOL Light. Zbl 1222.68370
McLaughlin, Sean
6
2006
Tool building requirements for an API to first-order solvers. Zbl 1272.68358
Grundy, Jim; Melham, Tom; Krstić, Sava; McLaughlin, Sean
1
2006
A proof-producing decision procedure for real arithmetic. Zbl 1135.03329
McLaughlin, Sean; Harrison, John
12
2005
all top 5

Cited by 147 Authors

6 Nipkow, Tobias
6 Paulson, Lawrence Charles
4 McLaughlin, Sean
3 Blanchette, Jasmin Christian
3 Böhme, Sascha
3 Hales, Thomas Callister
3 Kaliszyk, Cezary
3 Obua, Steven
3 Rabe, Florian
2 Aransay, Jesús
2 Bezdek, Károly
2 Chaudhuri, Kaustuv
2 Divasón, Jose
2 Grégoire, Benjamin
2 Muñoz, César A.
2 Narkawicz, Anthony Joseph
2 Urban, Josef
2 Weber, Tjark
2 Zumkeller, Roland
1 Adams, Mark
1 Adams, Mark F.
1 Akbarpour, Behzad
1 Alt, Helmut
1 Amjad, Hasan
1 Armand, Michaël
1 Avigad, Jeremy
1 Bancerek, Grzegorz
1 Barbosa, Haniel
1 Barsotti, Damián
1 Barthe, Gilles
1 Bauer, Gertrud
1 Besson, Frédéric
1 Bogoşel, Beniamin
1 Boldo, Sylvie
1 Bourne, David P.
1 Brock-Nannestad, Taus
1 Buchin, Kevin
1 Bucur, Dorin
1 Budzyńska, Katarzyna
1 Byliński, Czesław
1 Chaieb, Amine
1 Chaplick, Steven
1 Cheong, Otfried
1 Clancy, Kevin
1 Corneli, Joseph
1 Cornilleau, Pierre-Emmanuel
1 Dang, Tat Dat
1 Dutle, Aaron
1 Dyckhoff, Roy
1 Elser, Veit
1 Faure, Germain
1 Ferrari, Mauro
1 Fiorentini, Camillo
1 Fleury, Mathias
1 Fontaine, Pascal
1 Fox, Anthony C. J.
1 Fragalà, Ilaria
1 Fulla, Marlon
1 Gallego, Edisson
1 Ganesalingam, Mohan
1 Gómez-Ramírez, Danny Arlen de Jesús
1 Gowers, William Timothy
1 Grabowski, Adam
1 Gravel, Simon
1 Grayson, Daniel Richard
1 Guan, Yong
1 Gunther, Emmanuel
1 Harrison, John
1 Harrison, John R.
1 Harrison, John W.
1 Hoang, Le Truong
1 Holmes, Kathryn
1 Iancu, Mihnea
1 Ida, Tetsuo
1 Jackson, Paul B.
1 Jones, Robert B.
1 Kallus, Yoav
1 Keller, Chantal
1 Kindermann, Philipp
1 Knauer, Christian
1 Kohlhase, Michael
1 Konev, Boris
1 Köppe, Matthias
1 Korniłowicz, Artur
1 Krstic, Sava A.
1 Kuncak, Viktor
1 Lakhnech, Yassine
1 Lángi, Zsolt
1 Lawrence, John C.
1 Lelay, Catherine
1 Lewis, Robert Y.
1 Li, Liming
1 Li, Wenda
1 Li, Yongdong
1 Lisitsa, Alexei
1 Magron, Victor
1 Marin, Sonia
1 Matuszewski, Roman
1 Melquiond, Guillaume
1 Musin, Oleg R.
...and 47 more Authors

Citations by Year