7 papers
When Types Intersect and Effects Get Handled
Stefano Catozi, Ugo Dal Lago, Taro Sekiyama
We introduce a novel intersection type system for a -calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties o…
Powerdomains and nondeterminism in synthetic domain theory
Yue Niu, Taro Sekiyama
Synthetic domain theory is an axiomatization of domain theory within a constructive universe of sets such that all definable maps between domains are continuous. In this paper we c…
Validated Code Translation for Projects with External Libraries
Hanliang Zhang, Arindam Sharma, Cristina David +5
Large Language Models (LLMs) have shown promise for program translation, particularly for migrating systems code to memory-safe languages such as Rust. However, existing approaches…
A Category-Theoretic Framework for Dependent Effect Systems
Satoshi Kura, Marco Gaboardi, Taro Sekiyama +1
Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfu…
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
Kazuki Watanabe, Mayuko Kori, Taro Sekiyama +2
We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a…
Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination
Takamasa Okudono, Masaki Waga, Taro Sekiyama +1
Active learning of finite automata has been vigorously pursued for the purposes of analysis and explanation of black-box systems. In this paper, we study an L*-style learning algor…