Developments in Formal Proofs

Thomas C. Hales

Type: Preprint

Publication Date: 2014-01-01

Citations: 4

DOI: https://doi.org/10.48550/arxiv.1408.6474

View Publication

Locations

arXiv (Cornell University) - View - PDF
DataCite API - View

Similar Works

Action	Title	Year	Authors
+	Developments in Formal Proofs	2014	Thomas C. Hales
+	Reliably Reproducing Machine-Checked Proofs with the Coq Platform	2022	Karl Palmskog E. ̃Tassi Théo Zimmermann
+	Comparison of Two Theorem Provers: Isabelle/HOL and Coq	2018	Artem Yushkovskiy
+	Comparison of Two Theorem Provers: Isabelle/HOL and Coq.	2018	Artem Yushkovskiy Stavros Tripakis
+	From LCF to Isabelle/HOL	2019	Lawrence C. Paulson Tobias Nipkow Makarius Wenzel
+ PDF Chat	From LCF to Isabelle/HOL	2019	Lawrence C. Paulson Tobias Nipkow Makarius Wenzel
+ PDF Chat	Proust: A Nano Proof Assistant	2016	Prabhakar Ragde
+ PDF Chat	General Automation in Coq through Modular Transformations	2021	Valentin Blot Louise Dubois de Prisque Chantal Keller Pierre Vial
+	General Automation in Coq through Modular Transformations	2021	Valentin Blot Louise Dubois de Prisque Chantal Keller Pierre Vial
+	Isabelle: The Next 700 Theorem Provers	1993	Lawrence C. Paulson
+	Isabelle technology for the Archive of Formal Proofs.	2019	Makarius Wenzel
+ PDF Chat	Teaching Higher-Order Logic Using Isabelle	2024	Simon Tobias Lund Jørgen Villadsen
+ PDF Chat	Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started	2020	Angeliki Koutsoukou-Argyraki
+	QED at Large: A Survey of Engineering of Formally Verified Software	2019	Talia Ringer Karl Palmskog Ilya Sergey Milos Gligoric Zachary Tatlock
+	Exposé Bourbaki 1086 : Developments in formal proofs	2018	Thomas C. Hales
+ PDF Chat	QED at Large: A Survey of Engineering of Formally Verified Software	2019	Talia Ringer Karl Palmskog Ilya Sergey Milos Gligoric Zachary Tatlock
+ PDF Chat	A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving	2012	Freek Wiedijk
+	Interaction with Formal Mathematical Documents in Isabelle/PIDE	2019	Makarius Wenzel
+	Interaction with Formal Mathematical Documents in Isabelle/PIDE	2019	Makarius Wenzel
+	Formal Proof of Higman's Lemma on Isabelle/HOL	2012	Mizuhito Ogawa

Works That Cite This (3)

Action	Title	Year	Authors
+ PDF Chat	Book Review: Dense sphere packings: a blueprint for formal proofs	2015	Jeffrey C. Lagarias
+ PDF Chat	Mathematics and the formal turn	2024	Jeremy Avigad
+ PDF Chat	Goal Translation for a Hammer for Coq (Extended Abstract)	2016	Łukasz Czajka Cezary Kaliszyk

Works Cited by This (0)

Action	Title	Year	Authors