An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing. - Reynald Affeldt; Kazuhiko Sakaguchi (J. Formaliz. Reason., 2014)

Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. - Reynald Affeldt; Cyril Cohen; Marie Kerjean; Assia Mahboubi; Damien Rouhling; Kazuhiko Sakaguchi (IJCAR (2), 2020)

Validating Mathematical Structures. - Kazuhiko Sakaguchi (IJCAR (2), 2020)

Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). - Cyril Cohen; Kazuhiko Sakaguchi; Enrico Tassi (FSCD, 2020)

Program extraction for mutable arrays. - Kazuhiko Sakaguchi (Sci. Comput. Program., 2020)

Reflexive Tactics for Algebra, Revisited. - Kazuhiko Sakaguchi (ITP, 2022)

A bargain for mergesorts (functional pearl) - How to prove your mergesort correct and stable, almost for free. - Cyril Cohen; Kazuhiko Sakaguchi (CoRR, 2024)