zbMATH — the first resource for mathematics

Typing a core binary-field arithmetic in a light logic. (English) Zbl 1367.68050
Peña, Ricardo (ed.) et al., Foundational and practical aspects of resource analysis. Second international workshop, FOPARA 2011, Madrid, Spain, May 19, 2011. Revised selected papers. Berlin: Springer (ISBN 978-3-642-32494-9/pbk). Lecture Notes in Computer Science 7177, 19-35 (2012).
Summary: 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.
For the entire collection see [Zbl 1250.68046].
Reviewer: Reviewer (Berlin)

68N18 Functional programming and lambda calculus
03B70 Logic in computer science
Full Text: DOI