Pozvánka na přednášku semináře

  • Igor Sedlár (ICS CAS):

    One-sorted Kleene algebra with tests

    18.05.2022 16:00Místnost 318 (live) and streamed via Zoom @ Ústav informatiky
    Pod Vodárenskou věží 2
    Praha, 182 00
    Seminář aplikované matematické logiky

    Kleene algebra with tests, KAT, is a simple two-sorted algebraic framework for verifying properties of propositional while programs. One-sorted alternatives to KAT have been explored, mainly in connection with applications in automated program verification. A well known example of this approach is Kleene algebra with domain, KAD. A generalization of KAD called one-sorted Kleene algebra with tests, OneKAT, was recently proposed by the author in collaboration with J. Wannenburg. In this paper we show that KAT can be transformed into a flexible one-sorted framework that retains all natural properties of KAT. This framework, called Kleene algebra with test operators, is based on the idea of extending Kleene algebra with a set of test operators such that the set of images of the multiplicative unit under test operators generates a Boolean algebra of tests.

Předchozí přednášky