3 papers
cs.PL2026
Prophecy-Based Automated Verification of Message-Passing Programs
Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi +2
We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) s…
cs.PL2026
Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
Yusuke Matsushita, Hiromi Ishii
A promising approach to unifying functional and imperative programming paradigms is to localize mutation using linear or affine types. Haskell, a purely functional language, was re…
cs.PL2026
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays
Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga +1
Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT -- a type syst…