Talk "Iteration Calculus"

by Benjamin Lucien Kaminski

Fri, 01 November 2024 at 03:15 pm in Crete, Greece

Joint work with: Kevin Batz, Lucas Kehrer

Abstract: We introduce iteration calculus, a modal logic type of system for reasoning about fixed points of monotone endofunctions on complete lattices. Unlike systems such as mu-calculus, iteration calculus does not feature fixed point operators. Instead, it allows to reason about the existence of fixed points. For instance, we can prove theorems like the Kleene fixed point theorem, the more general Tarski-Kantorovich principle, or Park induction directly within iteration calculus.