3 papers
cs.LO2024
A bargain for mergesorts -- How to prove your mergesort correct and stable, almost for free
Cyril Cohen, Kazuhiko Sakaguchi
We present a novel characterization of stable mergesort functions using relational parametricity, and show that it implies the functional correctness of mergesort. As a result, one…
cs.PL2022
Reflexive tactics for algebra, revisited
Kazuhiko Sakaguchi
Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology i…
cs.PL2020
Validating Mathematical Structures
Kazuhiko Sakaguchi
Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in…