A Formalization of Dedekind Domains and Class Groups of Global Fields (English)
Free access
- New search for: Baanen, Anne
- Further information on Baanen, Anne:
-
https://orcid.org/0000-0001-8497-3683
- New search for: Dahmen, Sander R.
- Further information on Dahmen, Sander R.:
-
https://orcid.org/0000-0002-0014-0789
- New search for: Narayanan, Ashvni
- Further information on Narayanan, Ashvni:
-
https://orcid.org/0000-0003-2777-4228
- New search for: Nuccio Mortarino Majno di Capriglio, Filippo A. E.
- Further information on Nuccio Mortarino Majno di Capriglio, Filippo A. E.:
-
https://orcid.org/0000-0002-5318-9869
- New search for: Baanen, Anne
- Further information on Baanen, Anne:
-
https://orcid.org/0000-0001-8497-3683
- New search for: Dahmen, Sander R.
- Further information on Dahmen, Sander R.:
-
https://orcid.org/0000-0002-0014-0789
- New search for: Narayanan, Ashvni
- Further information on Narayanan, Ashvni:
-
https://orcid.org/0000-0003-2777-4228
- New search for: Nuccio Mortarino Majno di Capriglio, Filippo A. E.
- Further information on Nuccio Mortarino Majno di Capriglio, Filippo A. E.:
-
https://orcid.org/0000-0002-5318-9869
- New search for: Cohen, Liron
- Further information on Cohen, Liron:
-
https://orcid.org/0000-0002-6608-3000
- New search for: Kaliszyk, Cezary
- Further information on Kaliszyk, Cezary:
-
https://orcid.org/0000-0002-8273-6059
In:
LIPIcs, Volume 193, ITP 2021
: 12th International Conference on Interactive Theorem Proving (ITP 2021)
;
193
;
5:1-5:19
;
2021
-
ISBN:
-
ISSN:
- Conference paper / Electronic Resource
-
Title:A Formalization of Dedekind Domains and Class Groups of Global Fields
-
Contributors:Baanen, Anne ( author ) / Dahmen, Sander R. ( author ) / Narayanan, Ashvni ( author ) / Nuccio Mortarino Majno di Capriglio, Filippo A. E. ( author ) / Cohen, Liron ( editor ) / Kaliszyk, Cezary ( editor )
-
Published in:LIPIcs, Volume 193, ITP 2021 : 12th International Conference on Interactive Theorem Proving (ITP 2021) ; 193 ; 5:1-5:19Leibniz International Proceedings in Informatics (LIPIcs) ; 193 ; 5:1-5:19
-
Publisher:
- New search for: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
-
Publication date:2021-06-21
-
Size:19 pages , 793308 byte
-
Remarks:LIPIcs, Vol. 193, 12th International Conference on Interactive Theorem Proving (ITP 2021), pages 5:1-5: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
-
The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper)Myreen, Magnus O. et al. | 2021
- 2
-
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk)Polikarpova, Nadia et al. | 2021
- 3
-
Bounded-Deducibility Security (Invited Paper)Popescu, Andrei / Bauereiss, Thomas / Lammich, Peter et al. | 2021
- 4
-
A Graphical User Interface Framework for Formal VerificationAyers, Edward W. / Jamnik, Mateja / Gowers, W. T. et al. | 2021
- 5
-
A Formalization of Dedekind Domains and Class Groups of Global FieldsBaanen, Anne / Dahmen, Sander R. / Narayanan, Ashvni / Nuccio Mortarino Majno di Capriglio, Filippo A. E. et al. | 2021
- 6
-
A Formally Verified Checker for First-Order ProofsBaek, Seulkee et al. | 2021
- 7
-
Value-Oriented Legal Argumentation in Isabelle/HOLBenzmüller, Christoph / Fuenmayor, David et al. | 2021
- 8
-
Unsolvability of the Quintic Formalized in Dependent Type TheoryBernard, Sophie / Cohen, Cyril / Mahboubi, Assia / Strub, Pierre-Yves et al. | 2021
- 9
-
Itauto: An Extensible Intuitionistic SAT SolverBesson, Frédéric et al. | 2021
- 10
-
Verified Progress Tracking for Timely DataflowBrun, Matthias / Decova, Sára / Lattuada, Andrea / Traytel, Dmitriy et al. | 2021
- 11
-
Syntactic-Semantic Form of Mizar ArticlesByliński, Czesław / Korniłowicz, Artur / Naumowicz, Adam et al. | 2021
- 12
-
Homotopy Type Theory in IsabelleChen, Joshua et al. | 2021
- 13
-
Flexible Coinduction in AgdaCiccone, Luca / Dagnino, Francesco / Zucca, Elena et al. | 2021
- 14
-
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR AlgorithmCordwell, Katherine / Tan, Yong Kiam / Platzer, André et al. | 2021
- 15
-
Formalising a Turing-Complete Choreographic Language in CoqCruz-Filipe, Luís / Montesi, Fabrizio / Peressotti, Marco et al. | 2021
- 16
-
A Natural Formalization of the Mutilated Checkerboard Problem in NaprocheDe Lon, Adrian / Koepke, Peter / Lorenzen, Anton et al. | 2021
- 17
-
A Variant of Wagner’s Theorem Based on Combinatorial HypermapsDoczkal, Christian et al. | 2021
- 18
-
Formalized Haar Measurevan Doorn, Floris et al. | 2021
- 19
-
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-CalculusForster, Yannick / Kunze, Fabian / Smolka, Gert / Wuttke, Maximilian et al. | 2021
- 20
-
Mechanising Complexity Theory: The Cook-Levin Theorem in CoqGäher, Lennard / Kunze, Fabian et al. | 2021
- 21
-
Proving Quantum Programs CorrectHietala, Kesha / Rand, Robert / Hung, Shih-Han / Li, Liyi / Hicks, Michael et al. | 2021
- 22
-
Formalization of Basic Combinatorics on WordsHolub, Štěpán / Starosta, Štěpán et al. | 2021
- 23
-
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in CoqKirst, Dominik / Hermes, Marc et al. | 2021
- 24
-
Complete Bidirectional Typing for the Calculus of Inductive ConstructionsLennon-Bertrand, Meven et al. | 2021
- 25
-
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable NetworksLochbihler, Andreas et al. | 2021
- 26
-
A Formal Proof of Modal Completeness for Provability LogicMaggesi, Marco / Perini Brogi, Cosimo et al. | 2021
- 27
-
Formal Verification of Termination Criteria for First-Order Recursive FunctionsMuñoz, Cesar A. / Ayala-Rincón, Mauricio / Moscato, Mariano M. / Dutle, Aaron M. / Narkawicz, Anthony J. / Almeida, Ariane A. / Avelar, Andréia B. / M. Ferreira Ramos, Thiago et al. | 2021
- 28
-
Verified Double Sided Auctions for Financial MarketsNatarajan, Raja / Sarswat, Suneel / Singh, Abhishek Kr et al. | 2021
- 29
-
Reaching for the Star: Tale of a Monad in CoqNigron, Pierre / Dagand, Pierre-Évariste et al. | 2021
- 30
-
Specifying Message Formats with Contiguity TypesSlind, Konrad et al. | 2021
- 31
-
Proof Pearl : Playing with the Tower of Hanoi FormallyThéry, Laurent et al. | 2021
- 32
-
Verifying an HTTP Key-Value Server with Interaction Trees and VSTZhang, Hengchu / Honoré, Wolf / Koh, Nicolas / Li, Yao / Li, Yishuai / Xia, Li-Yao / Beringer, Lennart / Mansky, William / Pierce, Benjamin / Zdancewic, Steve et al. | 2021