Typing a Core Binary-Field Arithmetic in a Light Logic

We design a library for binary-ï¬ eld arithmetic and we supply a core application programming interface (API) completely developed in a formal system we introduce: Typeable Functional Assembly (TFA) which essentially is the system Dual Light Affine Logic (DLAL) introduced by Baillot and Terui and extended with a fix-point formula. TFA is a light type assignment system, in the sense that substructural rules on types of linear logic allow just to type functional programs with polynomial evaluation cost. As a consequence, we show the core of a functional programming setting for binary-field arithmetic with built-in polynomial complexity.