A Formalization of Forcing and the Unprovability of the Continuum Hypothesis (English)
Free access
- New search for: Han, Jesse Michael
- New search for: van Doorn, Floris
- New search for: Han, Jesse Michael
- New search for: van Doorn, Floris
- New search for: Harrison, John
- New search for: O'Leary, John
- New search for: Tolmach, Andrew
In:
LIPIcs, Volume 141, ITP 2019
: 10th International Conference on Interactive Theorem Proving (ITP 2019)
;
141
;
19:1-19:19
;
2019
-
ISBN:
-
ISSN:
- Conference paper / Electronic Resource
-
Title:A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
-
Contributors:Han, Jesse Michael ( author ) / van Doorn, Floris ( author ) / Harrison, John ( editor ) / O'Leary, John ( editor ) / Tolmach, Andrew ( editor )
-
Published in:LIPIcs, Volume 141, ITP 2019 : 10th International Conference on Interactive Theorem Proving (ITP 2019) ; 141 ; 19:1-19:19Leibniz International Proceedings in Informatics (LIPIcs) ; 141 ; 19:1-19:19
-
Publisher:
- New search for: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
-
Publication date:2019-09-05
-
Size:19 pages , 678869 byte
-
Remarks:LIPIcs, Vol. 141, 10th International Conference on Interactive Theorem Proving (ITP 2019), pages 19:1-19:19
-
ISBN:
-
ISSN:
-
DOI:
-
Type of media:Conference paper
-
Type of material:Electronic Resource
-
Language:English
-
Keywords:
-
Licence:
-
Source:
Table of contents conference proceedings
The tables of contents are generated automatically and are based on the data records of the individual contributions available in the index of the TIB portal. The display of the Tables of Contents may therefore be incomplete.
- 1
-
A Million Lines of Proof About a Moving Target (Invited Talk)Andronick, June et al. | 2019
- 2
-
What Makes a Mathematician Tick? (Invited Talk)Buzzard, Kevin et al. | 2019
- 3
-
An Increasing Need for Formality (Invited Talk)Dixon, Martin et al. | 2019
- 4
-
A Verified Compositional Algorithm for AI PlanningAbdulaziz, Mohammad / Gretton, Charles / Norrish, Michael et al. | 2019
- 5
-
Proving Tree Algorithms for Succinct Data StructuresAffeldt, Reynald / Garrigue, Jacques / Qi, Xuanrui / Tanaka, Kazunari et al. | 2019
- 6
-
Data Types as Quotients of Polynomial FunctorsAvigad, Jeremy / Carneiro, Mario / Hudon, Simon et al. | 2019
- 7
-
Primitive Floats in CoqBertholon, Guillaume / Martin-Dorel, Érik / Roux, Pierre et al. | 2019
- 8
-
A Certificate-Based Approach to Formally Verified ApproximationsBréhard, Florent / Mahboubi, Assia / Pous, Damien et al. | 2019
- 9
-
Higher-Order Tarski Grothendieck as a Foundation for Formal ProofBrown, Chad E. / Kaliszyk, Cezary / Pąk, Karol et al. | 2019
- 10
-
Generic Authenticated Data Structures, FormallyBrun, Matthias / Traytel, Dmitriy et al. | 2019
- 11
-
A Verified and Compositional Translation of LTL to Deterministic Rabin AutomataBrunner, Julian / Seidl, Benedikt / Sickert, Salomon et al. | 2019
- 12
-
Formalizing Computability Theory via Partial Recursive FunctionsCarneiro, Mario et al. | 2019
- 13
-
Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and IsabelleChen, Ran / Cohen, Cyril / Lévy, Jean-Jacques / Merz, Stephan / Théry, Laurent et al. | 2019
- 14
-
First-Order Guarded Coinduction in CoqCzajka, Łukasz et al. | 2019
- 15
-
Formalizing the Solution to the Cap Set ProblemDahmen, Sander R. / Hölzl, Johannes / Lewis, Robert Y. et al. | 2019
- 16
-
Nine Chapters of Analytic Number Theory in Isabelle/HOLEberl, Manuel et al. | 2019
- 17
-
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda CalculusForster, Yannick / Kunze, Fabian et al. | 2019
- 18
-
Formal Proof and Analysis of an Incremental Cycle Detection AlgorithmGuéneau, Armaël / Jourdan, Jacques-Henri / Charguéraud, Arthur / Pottier, François et al. | 2019
- 19
-
A Formalization of Forcing and the Unprovability of the Continuum HypothesisHan, Jesse Michael / van Doorn, Floris et al. | 2019
- 20
-
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOLHaslbeck, Maximilian P. L. / Lammich, Peter et al. | 2019
- 21
-
Virtualization of HOL4 in IsabelleImmler, Fabian / Rädle, Jonas / Wenzel, Makarius et al. | 2019
- 22
-
Generating Verified LLVM from Isabelle/HOLLammich, Peter et al. | 2019
- 23
-
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and DijkstraLammich, Peter / Nipkow, Tobias et al. | 2019
- 24
-
A Verified LL(1) Parser GeneratorLasser, Sam / Casinghino, Chris / Fisher, Kathleen / Roux, Cody et al. | 2019
- 25
-
Binary-Compatible Verification of Filesystems with ACL2Mehta, Mihir Parang / Cook, William R. et al. | 2019
- 26
-
Ornaments for Proof Reuse in CoqRinger, Talia / Yazdani, Nathaniel / Leo, John / Grossman, Dan et al. | 2019
- 27
-
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow SecuritySison, Robert / Murray, Toby et al. | 2019
- 28
-
Quantitative Continuity and Computable Analysis in CoqSteinberg, Florian / Théry, Laurent / Thies, Holger et al. | 2019
- 29
-
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in CoqTassi, Enrico et al. | 2019
- 30
-
Complete Non-Orders and Fixed PointsYamada, Akihisa / Dubut, Jérémy et al. | 2019
- 31
-
Verified Decision Procedures for Modal LogicsWu, Minchao / Goré, Rajeev et al. | 2019
- 32
-
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML ProgramsÅman Pohjola, Johannes / Rostedt, Henrik / Myreen, Magnus O. et al. | 2019
- 33
-
The DPRM Theorem in Isabelle (Short Paper)Bayer, Jonas / David, Marco / Pal, Abhik / Stock, Benedikt / Schleicher, Dierk et al. | 2019
- 34
-
Hammering Mizar by Learning Clause Guidance (Short Paper)Jakubův, Jan / Urban, Josef et al. | 2019
- 35
-
Declarative Proof Translation (Short Paper)Kaliszyk, Cezary / Pąk, Karol et al. | 2019
- 36
-
Formalization of the Domination Chain with Weighted Parameters (Short Paper)Severín, Daniel E. et al. | 2019