Skip to main navigation Skip to search Skip to main content

Certified Infinite Descent Criteria in Isabelle/HOL

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publication17th International Conference on Interactive Theorem Proving, ITP 2026
EditorsEkaterina Komendantskaya, Ekaterina Komendantskaya, Tobias Nipkow
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959774369
DOIs
Publication statusPublished - 16 Jul 2026
Event17th International Conference on Interactive Theorem Proving, ITP 2026 - Lisbon, Portugal
Duration: 26 Jul 202629 Jul 2026

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume382
ISSN (Print)1868-8969

Conference

Conference17th International Conference on Interactive Theorem Proving, ITP 2026
Country/TerritoryPortugal
CityLisbon
Period26/07/2629/07/26

Keywords

  • Büchi automata
  • Cyclic Proof
  • Infinite Descent
  • Size-Change termination

Cite this