Search dblp for Publications

export results for "toc:db/journals/afp/afp2022.bht:"

 download as .bib file

@article{DBLP:journals/afp/AmmerK22,
  author       = {Thomas Ammer and
                  Katharina Kreuzer},
  title        = {Number Theoretic Transform},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Number\_Theoretic\_Transform.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/AmmerK22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/BaksysK22,
  author       = {Mantas Baksys and
                  Angeliki Koutsoukou{-}Argyraki},
  title        = {Kneser's Theorem and the Cauchy-Davenport Theorem},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Kneser\_Cauchy\_Davenport.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/BaksysK22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/BayerDPS22,
  author       = {Jonas Bayer and
                  Marco David and
                  Abhik Pal and
                  Benedikt Stock},
  title        = {Digit Expansions},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Digit\_Expansions.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/BayerDPS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/BayerDSPMS22,
  author       = {Jonas Bayer and
                  Marco David and
                  Benedikt Stock and
                  Abhik Pal and
                  Yuri V. Matiyasevich and
                  Dierk Schleicher},
  title        = {Diophantine Equations and the {DPRM} Theorem},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/DPRM\_Theorem.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/BayerDSPMS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/BenzmullerFSS22,
  author       = {Christoph Benzm{\"{u}}ller and
                  David Fuenmayor and
                  Alexander Steen and
                  Geoff Sutcliffe},
  title        = {Automation of Boolos' Curious Inference in Isabelle/HOL},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Boolos\_Curious\_Inference\_Automated.html},
  timestamp    = {Wed, 12 Apr 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/BenzmullerFSS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Bortin22,
  author       = {Maksym Bortin},
  title        = {From {THE} {BOOK:} Two Squares via Involutions},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Involutions2Squares.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Bortin22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Brucker22,
  author       = {Achim D. Brucker},
  title        = {Nano {JSON:} Working with {JSON} formatted data in Isabelle/HOL and
                  Isabelle/ML},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Nano\_JSON.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Brucker22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/CordwellTP22,
  author       = {Katherine Cordwell and
                  Yong Kiam Tan and
                  Andr{\'{e}} Platzer},
  title        = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Quantifier\_Elimination\_Hybrid.html},
  timestamp    = {Wed, 12 Apr 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/CordwellTP22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Cremer22,
  author       = {Nils Cremer},
  title        = {Maximum Segment Sum},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Maximum\_Segment\_Sum.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Cremer22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Crighton22,
  author       = {Aaron Crighton},
  title        = {p-adic Fields and p-adic Semialgebraic Sets},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Padic\_Field.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Crighton22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/DalvitT22,
  author       = {Christian Dalvit and
                  Ren{\'{e}} Thiemann},
  title        = {A Verified Translation of Multitape Turing Machines into Singletape
                  Turing Machines},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Multitape\_To\_Singletape\_TM.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/DalvitT22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Dardinier22,
  author       = {Thibault Dardinier},
  title        = {Formalization of a Framework for the Sound Automation of Magic Wands},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Package\_logic.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Dardinier22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Dardinier22a,
  author       = {Thibault Dardinier},
  title        = {A Restricted Definition of the Magic Wand to Soundly Combine Fractions
                  of a Wand},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Combinable\_Wands.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Dardinier22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Dardinier22b,
  author       = {Thibault Dardinier},
  title        = {Unbounded Separation Logic},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Separation\_Logic\_Unbounded.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Dardinier22b.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/DelemazureDEIL22,
  author       = {Th{\'{e}}o Delemazure and
                  Tom Demeulemeester and
                  Manuel Eberl and
                  Jonas Israel and
                  Patrick Lederer},
  title        = {The Incompatibility of Strategy-Proofness and Representation in Party-Approval
                  Multi-Winner Elections},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/PAPP\_Impossibility.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/DelemazureDEIL22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Doty22,
  author       = {Matthew Doty},
  title        = {Risk-Free Lending},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Risk\_Free\_Lending.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Doty22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Doty22a,
  author       = {Matthew Doty},
  title        = {Birkhoff's Representation Theorem For Finite Distributive Lattices},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Birkhoff\_Finite\_Distributive\_Lattices.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Doty22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Doty22b,
  author       = {Matthew Doty},
  title        = {Class-based Classical Propositional Logic},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Propositional\_Logic\_Class.html},
  timestamp    = {Wed, 12 Apr 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Doty22b.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Eberl22,
  author       = {Manuel Eberl},
  title        = {A Proof from {THE} {BOOK:} The Partial Fraction Expansion of the Cotangent},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Cotangent\_PFD\_Formula.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Eberl22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Eberl22a,
  author       = {Manuel Eberl},
  title        = {The Sophomore's Dream},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Sophomores\_Dream.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Eberl22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Eberl22b,
  author       = {Manuel Eberl},
  title        = {P{\'{o}}lya's Proof of the Weighted Arithmetic-Geometric Mean
                  Inequality},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Weighted\_Arithmetic\_Geometric\_Mean.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Eberl22b.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Echenim22,
  author       = {Mnacho Echenim},
  title        = {Simultaneous diagonalization of pairwise commuting Hermitian matrices},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Commuting\_Hermitian.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Echenim22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Edmonds22,
  author       = {Chelsea Edmonds},
  title        = {Undirected Graph Theory},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Undirected\_Graph\_Theory.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Edmonds22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/EdmondsP22,
  author       = {Chelsea Edmonds and
                  Lawrence C. Paulson},
  title        = {Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Fishers\_Inequality.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/EdmondsP22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/FleuriotP22,
  author       = {Jacques D. Fleuriot and
                  Lawrence C. Paulson},
  title        = {Constructing the Reals as Dedekind Cuts of Rationals},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Dedekind\_Real.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/FleuriotP22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/From22,
  author       = {Asta Halkj{\ae}r From},
  title        = {A Naive Prover for First-Order Logic},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/FOL\_Seq\_Calc3.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/From22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/FromJ22,
  author       = {Asta Halkj{\ae}r From and
                  Frederik Krogsdal Jacobsen},
  title        = {A Sequent Calculus Prover for First-Order Logic with Functions},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/FOL\_Seq\_Calc2.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/FromJ22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/FromV22,
  author       = {Asta Halkj{\ae}r From and
                  J{\o}rgen Villadsen},
  title        = {Soundness and Completeness of Implicational Logic},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Implicational\_Logic.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/FromV22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/GuntherPTS22,
  author       = {Emmanuel Gunther and
                  Miguel Pagano and
                  Pedro S{\'{a}}nchez Terraf and
                  Mat{\'{\i}}as Steinberg},
  title        = {Transitive Models of Fragments of {ZFC}},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Transitive\_Models.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/GuntherPTS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/GuntherPTS22a,
  author       = {Emmanuel Gunther and
                  Miguel Pagano and
                  Pedro S{\'{a}}nchez Terraf and
                  Mat{\'{\i}}as Steinberg},
  title        = {The Independence of the Continuum Hypothesis in Isabelle/ZF},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Independence\_CH.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/GuntherPTS22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Guzman22,
  author       = {Laura P. Gamboa Guzman},
  title        = {Stalnaker's Epistemic Logic},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Stalnaker\_Logic.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Guzman22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/HirataMS22,
  author       = {Michikazu Hirata and
                  Yasuhiko Minamide and
                  Tetsuya Sato},
  title        = {Quasi-Borel Spaces},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Quasi\_Borel\_Spaces.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/HirataMS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/HofmeierK22,
  author       = {Paul Hofmeier and
                  Emin Karayel},
  title        = {Combinatorial Enumeration Algorithms},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Combinatorial\_Enumeration\_Algorithms.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/HofmeierK22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Ito22,
  author       = {Yosuke Ito},
  title        = {Actuarial Mathematics},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Actuarial\_Mathematics.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Ito22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Karayel22,
  author       = {Emin Karayel},
  title        = {Median Method},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Median\_Method.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Karayel22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Karayel22a,
  author       = {Emin Karayel},
  title        = {Interpolation Polynomials (in HOL-Algebra)},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Interpolation\_Polynomials\_HOL\_Algebra.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Karayel22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Karayel22b,
  author       = {Emin Karayel},
  title        = {Enumeration of Equivalence Relations},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Equivalence\_Relation\_Enumeration.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Karayel22b.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Karayel22c,
  author       = {Emin Karayel},
  title        = {Universal Hash Families},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Universal\_Hash\_Families.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Karayel22c.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Karayel22d,
  author       = {Emin Karayel},
  title        = {Formalization of Randomized Approximation Algorithms for Frequency
                  Moments},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Frequency\_Moments.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Karayel22d.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Karayel22e,
  author       = {Emin Karayel},
  title        = {A Combinator Library for Prefix-Free Codes},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Prefix\_Free\_Code\_Combinators.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Karayel22e.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Karayel22f,
  author       = {Emin Karayel},
  title        = {Finite Fields},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Finite\_Fields.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Karayel22f.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Keskin22,
  author       = {Ata Keskin},
  title        = {Sauer-Shelah Lemma},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Sauer\_Shelah\_Lemma.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Keskin22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Ketland22,
  author       = {Jeffrey Ketland},
  title        = {Boolos's Curious Inference in Isabelle/HOL},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Boolos\_Curious\_Inference.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Ketland22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Kirchner22,
  author       = {Daniel Kirchner},
  title        = {Abstract Object Theory},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/AOT.html},
  timestamp    = {Wed, 12 Apr 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Kirchner22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Klenze022,
  author       = {Tobias Klenze and
                  Christoph Sprenger},
  title        = {IsaNet: Formalization of a Verification Framework for Secure Data
                  Plane Protocols},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/IsaNet.html},
  timestamp    = {Sun, 04 Aug 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Klenze022.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Koller22,
  author       = {Lukas Koller},
  title        = {Knight's Tour Revisited Revisited},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Knights\_Tour.html},
  timestamp    = {Fri, 21 Jan 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Koller22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Koutsoukou-Argyraki22,
  author       = {Angeliki Koutsoukou{-}Argyraki and
                  Lawrence C. Paulson},
  title        = {The Pl{\"{u}}nnecke-Ruzsa Inequality},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Pluennecke\_Ruzsa\_Inequality.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Koutsoukou-Argyraki22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Koutsoukou-Argyraki22a,
  author       = {Angeliki Koutsoukou{-}Argyraki and
                  Lawrence C. Paulson},
  title        = {Khovanskii's Theorem},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Khovanskii\_Theorem.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Koutsoukou-Argyraki22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Koutsoukou-Argyraki22b,
  author       = {Angeliki Koutsoukou{-}Argyraki and
                  Mantas Baksys and
                  Chelsea Edmonds},
  title        = {The Balog-Szemer{\'{e}}di-Gowers Theorem},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Balog\_Szemeredi\_Gowers.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Koutsoukou-Argyraki22b.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Kreuzer22,
  author       = {Katharina Kreuzer},
  title        = {CRYSTALS-Kyber},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/CRYSTALS-Kyber.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Kreuzer22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Lauermann22,
  author       = {Nils Lauermann},
  title        = {Tur{\'{a}}n's Graph Theorem},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Turans\_Graph\_Theorem.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Lauermann22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Lochmann22,
  author       = {Alexander Lochmann},
  title        = {Reducing Rewrite Properties to Properties on Ground Terms},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Rewrite\_Properties\_Reduction.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Lochmann22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/LochmannF22,
  author       = {Alexander Lochmann and
                  Bertram Felgenhauer},
  title        = {First-Order Theory of Rewriting},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/FO\_Theory\_Rewriting.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/LochmannF22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/MarmsolerB22,
  author       = {Diego Marmsoler and
                  Achim D. Brucker},
  title        = {Isabelle/Solidity: {A} deep Embedding of Solidity in Isabelle/HOL},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Solidity.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/MarmsolerB22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/MerzT22,
  author       = {Stephan Merz and
                  Vincent Tr{\'{e}}lat},
  title        = {Correctness of a Set-based Algorithm for Computing Strongly Connected
                  Components of a Graph},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/SCC\_Bloemen\_Sequential.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/MerzT22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Noce22,
  author       = {Pasquale Noce},
  title        = {A Reuse-Based Multi-Stage Compiler Verification for Language {IMP}},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/IMP\_Compiler\_Reuse.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Noce22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Park22,
  author       = {Seung Hoon Park},
  title        = {A Formal {CHERI-C} Memory Model},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/CHERI-C\_Memory\_Model.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Park22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Paulson22,
  author       = {Lawrence C. Paulson},
  title        = {Irrational numbers from {THE} {BOOK}},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Irrationals\_From\_THEBOOK.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Paulson22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Paulson22a,
  author       = {Lawrence C. Paulson},
  title        = {Young's Inequality for Increasing Functions},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Youngs\_Inequality.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Paulson22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Paulson22b,
  author       = {Lawrence C. Paulson},
  title        = {Wetzel's Problem and the Continuum Hypothesis},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Wetzels\_Problem.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Paulson22b.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Paulson22c,
  author       = {Lawrence C. Paulson},
  title        = {Ackermann's Function Is Not Primitive Recursive},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Ackermanns\_not\_PR.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Paulson22c.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Raszyk22,
  author       = {Martin Raszyk},
  title        = {Multi-Head Monitoring of Metric Dynamic Logic},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/VYDRA\_MDL.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Raszyk22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Raszyk22a,
  author       = {Martin Raszyk},
  title        = {First-Order Query Evaluation},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Eval\_FO.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Raszyk22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/RaszykT22,
  author       = {Martin Raszyk and
                  Dmitriy Traytel},
  title        = {Making Arbitrary Relational Calculus Queries Safe-Range},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Safe\_Range\_RC.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/RaszykT22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Sachtleben22,
  author       = {Robert Sachtleben},
  title        = {Verified Complete Test Strategies for Finite State Machines},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/FSM\_Tests.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/Sachtleben22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Stark22,
  author       = {Eugene W. Stark},
  title        = {Residuated Transition Systems},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/ResiduatedTransitionSystem.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Stark22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/StevensS22,
  author       = {Lukas Stevens and
                  Bernhard St{\"{o}}ckl},
  title        = {Verification of Query Optimization Algorithms},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Query\_Optimization.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/StevensS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/SulejmaniEK22,
  author       = {Ujkan Sulejmani and
                  Manuel Eberl and
                  Katharina Kreuzer},
  title        = {The Hales-Jewett Theorem},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Hales\_Jewett.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/SulejmaniEK22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Thiemann22,
  author       = {Ren{\'{e}} Thiemann},
  title        = {Duality of Linear Programming},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/LP\_Duality.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Thiemann22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/Thiemann22a,
  author       = {Ren{\'{e}} Thiemann},
  title        = {Clique is not solvable by monotone circuits of polynomial size},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Clique\_and\_Monotone\_Circuits.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/Thiemann22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/ThiemannS22,
  author       = {Ren{\'{e}} Thiemann and
                  Lukas Schmidinger},
  title        = {The Generalized Multiset Ordering is NP-Complete},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Multiset\_Ordering\_NPC.html},
  timestamp    = {Wed, 22 Jun 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/afp/ThiemannS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/TothN22,
  author       = {Bal{\'{a}}zs T{\'{o}}th and
                  Tobias Nipkow},
  title        = {Real-Time Double-Ended Queue},
  journal      = {Arch. Formal Proofs},
  volume       = {2022},
  year         = {2022},
  url          = {https://www.isa-afp.org/entries/Real\_Time\_Deque.html},
  timestamp    = {Mon, 12 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/TothN22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.