SearcharxivSearch

arXiv subjects

Kentaro Kobayashi

Publications and source records attributed to Kentaro Kobayashi.

4 recordsLinked to original sources

Expressive power of one-shot control operators and coroutines

Control operators, such as exceptions and effect handlers, provide a means of representing computational effects in programs abstractly and modularly. While most theoretical studies have focused on multi-shot control operators, one-shot control operators---which restrict the use of captured continuations to at most once---are gaining attention for their balance between expressiveness and efficiency. This study aims to fill the gap. We present a mathematically rigorous comparison of the expressive power among one-shot control operators, including effect handlers, delimited continuations, and even asymmetric coroutines. Following previous studies on multi-shot control operators, we adopt Felleisen's macro-expressiveness as our measure of expressiveness. We verify the folklore that one-shot effect handlers and one-shot delimited-control operators can be macro-expressed by asymmetric coroutines, but not vice versa. We explain why a previous informal argument fails, and how to revise it to make a valid macro-translation. This is the extended version of a paper presented at APLAS 2025.

cs.PL

Expressive Power of One-Shot Control Operators and Coroutines

Control operators, such as exceptions and effect handlers, provide a means of representing computational effects in programs abstractly and modularly. While most theoretical studies have focused on multi-shot control operators, one-shot control operators -- which restrict the use of captured continuations to at most once -- are gaining attention for their balance between expressiveness and efficiency. This study aims to fill the gap. We present a mathematically rigorous comparison of the expressive power among one-shot control operators, including effect handlers, delimited continuations, and even asymmetric coroutines. Following previous studies on multi-shot control operators, we adopt Felleisen's macro-expressiveness as our measure of expressiveness. We verify the folklore that one-shot effect handlers and one-shot delimited-control operators can be macro-expressed by asymmetric coroutines, but not vice versa. We explain why a previous informal argument fails, and how to revise it to make a valid macro-translation.

cs.PL

StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs

Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate this problem, we propose a tool-assisted method for formally specifying and automatically verifying the correctness of statistical programs. In this method, programmers are required to annotate the source code of the statistical programs with the requirements for these methods. Through this annotation, they are reminded to check the requirements for statistical methods, including those that cannot be formally verified, such as the distribution of the unknown true population. Our software tool StatWhy automatically checks whether programmers have properly specified the requirements for the statistical methods, thereby identifying any missing requirements that need to be addressed. This tool is implemented using the Why3 platform to verify the correctness of OCaml programs that conduct statistical hypothesis testing. We demonstrate how StatWhy can be used to avoid common errors in various statistical hypothesis testing programs.

cs.SE

Determination of the Electronic Localized-to-Extended-State Transition Point around the Metal-to-Insulator Transition Region of Fluid Mercury Using the Framework of Multifractal Analysis

The metal-to-insulator transition and the presence of the disorder induced localization of electronic orbitals of fluid mercury (f-Hg) were investigated. The electronic structure of f-Hg was simulated by means of ab initio molecular dynamics. To see the behavior of the simulation size dependency of the electronic orbital, systems with different number of atoms were simulated. The size dependency of the multifractal measure of the electronic orbitals reversed with decreasing the density, which suggests there exists the extended-to-localized-state transition near the metal-to-insulator transition region of f-Hg.

cond-mat.mtrl-sci