Formalizing Computability Theory via Partial Recursive Functions (Englisch)
Freier Zugriff
- Neue Suche nach: Carneiro, Mario
- Weitere Informationen zu Carneiro, Mario:
- https://orcid.org/0000-0002-0470-5249
- Neue Suche nach: Carneiro, Mario
- Weitere Informationen zu Carneiro, Mario:
- https://orcid.org/0000-0002-0470-5249
- Neue Suche nach: Harrison, John
- Neue Suche nach: O'Leary, John
- Neue Suche nach: Tolmach, Andrew
In:
LIPIcs, Volume 141, ITP 2019
: 10th International Conference on Interactive Theorem Proving (ITP 2019)
;
141
;
12:1-12:17
;
2019
-
ISBN:
-
ISSN:
- Aufsatz (Konferenz) / Elektronische Ressource
-
Titel:Formalizing Computability Theory via Partial Recursive Functions
-
Beteiligte:Carneiro, Mario ( Autor:in ) / Harrison, John ( Herausgeber:in ) / O'Leary, John ( Herausgeber:in ) / Tolmach, Andrew ( Herausgeber:in )
-
Erschienen in:LIPIcs, Volume 141, ITP 2019 : 10th International Conference on Interactive Theorem Proving (ITP 2019) ; 141 ; 12:1-12:17Leibniz International Proceedings in Informatics (LIPIcs) ; 141 ; 12:1-12:17
-
Verlag:
- Neue Suche nach: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
-
Erscheinungsdatum:05.09.2019
-
Format / Umfang:17 pages , 493435 byte
-
Anmerkungen:LIPIcs, Vol. 141, 10th International Conference on Interactive Theorem Proving (ITP 2019), pages 12:1-12:17
-
ISBN:
-
ISSN:
-
DOI:
-
Medientyp:Aufsatz (Konferenz)
-
Format:Elektronische Ressource
-
Sprache:Englisch
-
Schlagwörter:
-
Lizenzbestimmungen:
-
Datenquelle:
Inhaltsverzeichnis Konferenzband
Die Inhaltsverzeichnisse werden automatisch erzeugt und basieren auf den im Index des TIB-Portals verfügbaren Einzelnachweisen der enthaltenen Beiträge. Die Anzeige der Inhaltsverzeichnisse kann daher unvollständig oder lückenhaft sein.
- 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