Page 53 - 8th European Congress of Mathematics ∙ 20-26 June 2021 ∙ Portorož, Slovenia ∙ Book of Abstracts
P. 53
INVITED SPEAKERS
[3] Leo de Moura, Sebastian Ullrich, and Dany Fabian. Lean theorem prover.
[4] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François
Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana
Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-
checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and
David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP
2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in
Computer Science, pages 163–179. Springer, 2013.
[5] Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong
Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen,
Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey
Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and
Roland Zumkeller. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5,
2017.
[6] E. G. H. Y. Landau. Grundlagen der Analysis. Chelsea Pub. Co., New York, NY, USA,
1965.
[7] Per Martin-Löf. An intuitionistic theory of types. In Giovanni Sambin and Jan M. Smith,
editors, Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford
Logic Guides, pages 127–172. Oxford University Press, 1998.
[8] Ulf Norell. Towards a practical programming language based on dependent type theory.
PhD thesis, Chalmers University of Technology, 2007.
[9] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for
Mathematics , Institute for Advanced Study, 2013.
[10] Coq Development Team. The Coq proof assistant reference manual, version 8.7.
[11] L. S. van Benthem Jutting. Checking Landau’s “Grundlagen” in the Automath system. In
Mathematical Centre Tracts, volume 83. Mathematisch Centrum, The Netherlands, 1979.
[12] D. T. van Daalen. A description of automath and some aspects of its language theory. In
Selected Papers on Automath, pages 101–126. North-Holland Pub. Co., Amsterdam, The
Netherlands, 1994.
[13] Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath: Univalent Math-
ematics, 2016.
[14] Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge Uni-
versity Press, 1925–1927.
51
[3] Leo de Moura, Sebastian Ullrich, and Dany Fabian. Lean theorem prover.
[4] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François
Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana
Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-
checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and
David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP
2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in
Computer Science, pages 163–179. Springer, 2013.
[5] Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong
Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen,
Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey
Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and
Roland Zumkeller. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5,
2017.
[6] E. G. H. Y. Landau. Grundlagen der Analysis. Chelsea Pub. Co., New York, NY, USA,
1965.
[7] Per Martin-Löf. An intuitionistic theory of types. In Giovanni Sambin and Jan M. Smith,
editors, Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford
Logic Guides, pages 127–172. Oxford University Press, 1998.
[8] Ulf Norell. Towards a practical programming language based on dependent type theory.
PhD thesis, Chalmers University of Technology, 2007.
[9] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for
Mathematics , Institute for Advanced Study, 2013.
[10] Coq Development Team. The Coq proof assistant reference manual, version 8.7.
[11] L. S. van Benthem Jutting. Checking Landau’s “Grundlagen” in the Automath system. In
Mathematical Centre Tracts, volume 83. Mathematisch Centrum, The Netherlands, 1979.
[12] D. T. van Daalen. A description of automath and some aspects of its language theory. In
Selected Papers on Automath, pages 101–126. North-Holland Pub. Co., Amsterdam, The
Netherlands, 1994.
[13] Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath: Univalent Math-
ematics, 2016.
[14] Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge Uni-
versity Press, 1925–1927.
51
