Takafumi Saikawa

16 papers B 4C 5Journal 7
YearRankTypeTitle / 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