1 citations · 1 across the 3 of their papers we have counts for
4 papers
Full Definability in a Profunctorial Model
Takeshi Tsukada, Kazuyuki Asada, Kengo Hirata
A semantic model enjoys full definability if every semantic element in the model is a denotation of some proof or program. Full definability indicates that the model captures progr…
RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka +1
Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as d…
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
Kengo Hirata, Chris Heunen
Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources.…
Notes on Lax Ends
Kengo Hirata
In enriched category theory, the notion of extranatural transformations is more fundamental than that of ordinary natural transformations, and the ends, the universal extranatural…