From the 1 of 4 linked papers with an AI index.
4 papers
From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory
Shuo Deng, Kenneth W. Shum
The paper describes an ongoing effort to formalize a university-level probability textbook in the Lean theorem prover, creating a machine‑checked companion and reusable probability…
Multichannel Conflict-Avoiding Codes for Expanded Scenarios
Tsai-Lien Wong, Kangkang Xu, Yuan-Hsun Lo +2
A conflict-avoiding code (CAC) of length L and weight w is used for deterministic multiple-access without feedback. When the number of simultaneous active users is less than or equ…
Regenerating codes with minimal disk I/O cost achieving optimal tradeoff between storage and repair bandwidth
Minhan Gao, Kenneth Shum
Regenerating codes achieve the fundamental tradeoff between storage efficiency and repair bandwidth in distributed storage systems. Beyond these two parameters, disk I/O cost is an…
Efficient encoding and decoding algorithm for a class of perfect single-deletion-correcting permutation codes
Minhan Gao, Kenneth W. Shum
A permutation code is a nonlinear code whose codewords are permutation of a set of symbols. We consider the use of permutation code in the deletion channel, and consider the symbol…