]>
Kazuhiko Sakaguchi
Kazuhiko Sakaguchi (坂口和彦)
Publications
Speakers are underlined.
Reynald Affeldt , Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: a case study in functional analysis. IJCAR 2020LNAI , vol. 12167, pp. 3-20, 2020. [doi , preprint , slides and accompanying materials ]Kazuhiko Sakaguchi . Validating Mathematical Structures. IJCAR 2020, LNAI, vol. 12167, pp. 138-157, 2020. [doi , preprint , slides , accompanying materials ]Cyril Cohen , Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi (System Description). FSCD 2020LIPIcs , vol. 167, pp. 34:1-34:21, 2020. [doi , preprint , GitHub ]Kazuhiko Sakaguchi. Program Extraction for Mutable Arrays. Science of Computer Programming , vol. 191, pp. 102372, 2020. [doi , preprint ]
Kazuhiko Sakaguchi . Program Extraction for Mutable Arrays. FLOPS 2018LNCS , vol. 10818, pp. 51-67, 2018. [doi ]Kazuhiko Sakaguchi and Yukiyoshi Kameyama. Efficient Finite-Domain Function Library for the Coq Proof Assistant. IPSJ Transactions on ProgrammingIPSJ Digital Library , author's version , slides , accompanying materials ]
Reynald Affeldt and Kazuhiko Sakaguchi. An intrinsic encoding of a subset of C and its application to TLS network packet processing. Journal of Formalized Reasoning , vol. 7, no. 1, pp. 63-104, 2014. [doi , project page ]
Thesis
坂口和彦「定理証明器 Coq の効率的な有限ドメイン関数ライブラリ」 平成28年度 筑波大学大学院博士前期課程 システム情報工学研究科 修士論文
坂口和彦「型付きλ計算の強正規化定理の形式化」 平成26年度 筑波大学情報科学類 卒業研究論文 [slides , revised version , GitHub ]
Talks and posters
Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi , Laurent Théry, and Anton Trunov. Porting the Mathematical Components library to Hierarchy Builder. The Coq Workshop 2021 .
Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi . Hierarchy Builder. The Coq Workshop 2020 .
Xavier Allamigeon, Cyril Cohen, Kazuhiko Sakaguchi , and Pierre-Yves Strub. A hierarchy of ordered types in Mathematical Components. The Coq Workshop 2020.
Kazuhiko Sakaguchi . Validating Mathematical Structures. PPL 2020Kazuhiko Sakaguchi . Validating Mathematical Structures. TPP 2019Kazuhiko Sakaguchi . Validating Mathematical Structures. The Coq Workshop 2019 .坂口和彦 「置換の自動証明タクティク」(PPL 2018 C3). [poster ]Kazuhiko Sakaguchi . Program Extraction for Mutable Arrays. TPP 2017 .Kazuhiko Sakaguchi . Program Extraction for Mutable Arrays. TABLEAUX /FroCoS /ITP 2017poster , GitHub ]坂口和彦 「定理証明器 Coq の効率的な有限ドメイン関数ライブラリ」(TPP 2016 ).坂口和彦 ，亀山幸義「Coq/SSReflect の extraction の改善」(PPL 2016 C3). [poster ]坂口和彦 「プレスバーガー算術の決定可能性 - 有限オートマトンを使う証明の形式化」 (TPP 2015 ). [slides ]坂口和彦 「並列代入に対する代入補題の自動証明」(PPL 2015 C1) [slides , author's version , GitHub ]Kazuhiko Sakaguchi . Formalizing Strong Normalization Proofs. TPP 2014 . [slides ]Kazuhiko Sakaguchi . Interactive Stack-oriented Programming in the Coq Proof Assistant. IPSJ-PRO 99 . [slides , paper ]アフェルトレナルド ，坂口和彦 「Coq による C プログラムの検証基盤のデモ」(PPL 2014 C3).坂口和彦 「線形合同法の周期 - TAoCP 3.2.1.2の形式化」(TPP 2013 ). [slides ]アフェルトレナルド ，坂口和彦 「Coq によるセキュリティプロトコルの実装の検証」(日本ソフトウェア科学会第30回大会 一般デモ・ポスター発表).Reynald Affeldt , Kazuhiko Sakaguchi. First Building Blocks for Implementations of Security Protocols Verified in Coq. The Coq Workshop 2013 .坂口和彦 「Coq による PostScript プログラミング」(PPL 2013 C3).坂口和彦 「Coq による PostScript プログラミング」(TPP 2012 ).
Academic services
Grants, awards, etc.
Poster Award of PPL 2018 .
IPSJ Computer Science Research Award for Young Scientists , 2017.JSPS JASSO Provost Award of the Graduate School of Systems and Information Engineering , University of Tsukuba, 2017.PLMW ICFP 2016Provost Award of the School of Informatics , University of Tsukuba, 2015.
Advancing Researcher Experience Program , University of Tsukuba, 2012 and 2013.Outstanding Performance Award (優秀賞) of the Special Exercise in Information Science II , College of Information Science, University of Tsukuba, 2013.