Takafumi Saikawa

16 papers B 4C 5Journal 7

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A practical formalization of monadic equational reasoning in dependent-type theory. J. Funct. Program. Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2025	C	`conf`	An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols. FORTE Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2025	B	`conf`	Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. ITP Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa
2024	B	`conf`	Robust Mean Estimation by All Means (Short Paper). ITP Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann
2024	B	`conf`	Typed Compositional Quantum Computation with Lenses. ITP Jacques Garrigue, Takafumi Saikawa
2023	J	`jnl`	A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory. CoRR Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2023	J	`jnl`	Typed compositional quantum computation with lenses. CoRR Jacques Garrigue, Takafumi Saikawa
2021	J	`jnl`	A trustful monad for axiomatic reasoning with probability and nondeterminism. J. Funct. Program. Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
2020	J	`jnl`	A Library for Formalization of Linear Error-Correcting Codes. J. Autom. Reason. Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2020	J	`jnl`	A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism. CoRR Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
2020	C	`conf`	Formal Adventures in Convex and Conical Spaces. CICM Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2020	J	`jnl`	Formal Adventures in Convex and Conical Spaces. CoRR Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2020	C	`conf`	Formal Verification and Code-Generation of Mersenne-Twister Algorithm. ISITA Takafumi Saikawa, Kazunari Tanaka, Kensaku Tanaka
2019	B	`conf`	A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. MPC Reynald Affeldt, David Nowak, Takafumi Saikawa
2018	C	`conf`	Examples of Formal Proofs about Data Compression. ISITA Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2016	C	`conf`	Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. ISITA Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa