Showing 1–2 of 2 results for author: Üsküplü, E

Formalizing two-level type theory with cofibrant exo-nat

Authors: Elif Uskuplu

Abstract: This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory such as Agda. The difference from prior works is that these proofs do not assume any abuse of notation, providing us with more direct formalization. Moreover, some new notions, such as function extensionality for cofibrant t… ▽ More This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory such as Agda. The difference from prior works is that these proofs do not assume any abuse of notation, providing us with more direct formalization. Moreover, some new notions, such as function extensionality for cofibrant types, are introduced. The necessity of such notions arises during the task of formalization. In addition, we provide some novel results about inductive types using cofibrant exo-nat, the natural number type at the non-fibrant level. While emphasizing the necessity of this axiom by citing new applications as justifications, we also touch upon the semantic aspect of the theory by presenting various models that satisfy this axiom. △ Less

Submitted 17 September, 2023; originally announced September 2023.

QC-LDPC Codes from Difference Matrices and Difference Covering Arrays

Authors: Diane Donovan, Asha Rao, Elif Üsküplü, E. Ş. Yazıcı

Abstract: We give a framework for generalizing LDPC code constructions that use Transversal Designs or related structures such as mutually orthogonal Latin squares. Our construction offers a broader range of code lengths and codes rates. Similar earlier constructions rely on the existence of finite fields of order a power of a prime. In contrast the LDPC codes constructed here are based on difference matric… ▽ More We give a framework for generalizing LDPC code constructions that use Transversal Designs or related structures such as mutually orthogonal Latin squares. Our construction offers a broader range of code lengths and codes rates. Similar earlier constructions rely on the existence of finite fields of order a power of a prime. In contrast the LDPC codes constructed here are based on difference matrices and difference covering arrays, structures available for any order $a$. They satisfy the RC constraint and have, for $a$ odd, length $a^2$ and rate $1-\frac{4a-3}{a^2}$, and for $a$ even, length $a^2-a$ and rate at least $1-\frac{4a-6}{a^2-a}$. When $3$ does not divide $a$, these LDPC codes have stop** distance at least $8$. When $a$ is odd and both $3$ and $5$ do not divide $a$, our construction delivers an infinite family of QC-LDPC codes with minimum distance at least $10$. The simplicity of the construction allows us to theoretically verify these properties and analytically determine lower bounds for the minimum distance and stop** distance of the code. The BER and FER performance of our codes over AWGN (via simulation) is at the least equivalent to codes constructed previously, while in some cases significantly outperforming them. △ Less

Submitted 1 May, 2022; originally announced May 2022.