POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Tue 21 Jan 2025 16:18 - 16:36 at Patty Cake - Analysis Techniques

TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.

Tue 21 Jan

Displayed time zone: Mountain Time (US & Canada) change

16:00 - 17:30
Analysis TechniquesTPSA at Patty Cake
16:00
18m
Talk
Distributed transactions over mergeable types: A meta-theory for 5G control-plane protocol verification
TPSA
Prasanth Prahladan University of Colorado Boulder
16:18
18m
Talk
Domain Reasoning In TopKAT: Reduction and Completeness
TPSA
Cheng Zhang University College London (UCL), Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Marco Gaboardi Boston University
16:36
18m
Talk
From Traces to Program Incorrectness: A Type-Theoretic Approach
TPSA
Yongwei Yuan Purdue University, Zhe Zhou Purdue University, Julia Belyakova Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
16:54
18m
Talk
Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
TPSA
Naifeng Zhang Carnegie Mellon University, Sanil Rao Carnegie Mellon University, Mike Franusich SpiralGen, Inc., Franz Franchetti Carnegie Mellon University, USA
17:12
18m
Talk
Concurrent Quantum Separation Logic for Fine-Grained Parallelism
TPSA
Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University