We design a library for binary-field 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.
Cesena, E., Pedicini, M., Roversi, L. (2012). Typing a Core Binary-Field Arithmetic in a Light Logic. In M.v.E.a.O.S. Ricardo Peña (a cura di), Foundational and Practical Aspects of Resource Analysis Second International Workshop, FOPARA 2011, Madrid, Spain, May 19, 2011, Revised Selected Papers (pp. 19-35). New York Dordrecht Heidelberg London : Springer [10.1007/978-3-642-32495-6_2].
Typing a Core Binary-Field Arithmetic in a Light Logic
PEDICINI, MARCO;
2012-01-01
Abstract
We design a library for binary-field 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
