Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Sakayori, Ken"'
Autor:
Sakayori, Ken, Sangiorgi, Davide
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $\lambda$-calculus, the process representations yield (at best) non-extensional $\lambda $-theories (i.e., $\beta$ rule holds
Externí odkaz:
http://arxiv.org/abs/2405.03536
Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type syste
Externí odkaz:
http://arxiv.org/abs/2312.06455
Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recently been applied to address this issue, but the existing approaches were
Externí odkaz:
http://arxiv.org/abs/2310.20430
Autor:
Shoshi, Tsubasa, Ishikawa, Takuma, Kobayashi, Naoki, Sakayori, Ken, Sato, Ryosuke, Tsukada, Takeshi
We propose an automated method for proving termination of $\pi$-calculus processes, based on a reduction to termination of sequential programs: we translate a $\pi$-calculus process to a sequential program, so that the termination of the latter impli
Externí odkaz:
http://arxiv.org/abs/2109.00311
Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of
Externí odkaz:
http://arxiv.org/abs/2108.07642
Autor:
Sakayori, Ken, Sangiorgi, Davide
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure λ-calculus, the process representations yield (at best) non-extensional λ-theories (i.e., β rule holds, whereas η does no
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::2eaa4bd7fd8f1ecd45712147728ea34b
https://hal.science/hal-04081885/file/main.pdf
https://hal.science/hal-04081885/file/main.pdf
Autor:
Sakayori, Ken, Tsukada, Takeshi
The quest for logical or categorical foundations of the π-calculus (not limited to session-typed variants) remains an important challenge. A categorical type theory correspondence for a variant of the i/o-typed π-calculus was recently revealed by S
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e435e965c9df6fd8bf74596144367a89
Autor:
Sakayori, Ken-ichi, Matsui, Yasunori, Abe, Hiroyuki, Nakamura, Eiji, Kenmoku, Mikihiko, Hara, Tomoyuki, Ishikawa, Daisuke, Kokubu, Akihiro, Hirota, Ken-ichi, Takuro Ikeda, Takuro Ikeda
Publikováno v:
Japanese Journal of Applied Physics; September 1995, Vol. 34 Issue: 9 p5443-5443, 1p
