检索结果-内蒙古大学图书馆

Light combinators for finite fields arithmetic

SCIENCE OF COMPUTER PROGRAMMING 2015年第Part3期111卷 365-394页

作者： Canavese, D. Cesena, E. Ouchary, R. Pedicini, M. Roversi, L. Politecn Torino Dipartimento Automat & Informat I-10129 Turin Italy Theneeds Inc San Francisco CA USA Univ Rome Tre Dipartimento Matemat & Fis I-00146 Rome Italy Univ Turin Dipartimento Informat I-10149 Turin Italy

This work completes the definition of a library which provides the basic arithmetic operations in binary finite fields as a set of functional terms with very specific features. Such a functional terms have type in Typeable Functional Assembly (TFA). TFA is an extension of Dual Light Affine Logic (DLAL). DIAL is a type assignment designed under the prescriptions of implicit computational complexity (ICC), which characterises polynomial time costing computations. We plan to exploit the functional programming patterns of the terms in the library to implement cryptographic primitives whose running-time efficiency can be obtained by means of the least hand-made tuning as possible. We propose the library as a benchmark. It fixes a kind of lower bound on the difficulty of writing potentially interesting low cost programs inside languages that can express only computations with predetermined complexity. In principle, every known and future ICC compliant programming language for polynomially costing computations should supply a simplification over the encoding of the library we present, or some set of combinators of comparable interest and difficulty. We finally report on the applicative outcome that our library has and which is a reward we get by programming in the very restrictive scenario that TFA provides. The term of TFA which encodes the inversion in binary fields suggested us a variant of a known and efficient imperative implementation of the inversion itself given by Fong. Our variant, can outperform Fong's implementation of inversion on specific hardware architectures. (C) 2015 Elsevier B.V. All rights reserved.

关键词： Lambda calculus Finite fields arithmetic Type assignments implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

Linear dependent types in a call-by-value scenario

引用

SCIENCE OF COMPUTER PROGRAMMING 2014年 84卷 77-100页

作者： Dal Lago, Ugo Petit, Barbara INRIA Sophia Antipolis Bologna Italy Univ Bologna I-40126 Bologna Italy INRIA Rhone Alpes Grenoble France

Linear dependent types were introduced recently (Dal Lago and Gaboardi, 2012) [26] as a formal system that allows to precisely capture both the extensional behavior and the time complexity of A-terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to call-by-value computation. A system of linear dependent types for Plotkin's PCF is introduced, called dlPCF(v), whose types reflect the complexity of evaluating terms in the CEK machine. dlPCF(v) is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behavior of terms can be derived, provided all true index term inequalities can be used as assumptions. (C) 2013 Elsevier B.V. All rights reserved.

关键词： complexity analysis implicit computational complexity Type systems Linear logic

来源：评论

学校读者我要写书评

暂无评论

On bounding space usage of streams using interpretation analysis

引用

SCIENCE OF COMPUTER PROGRAMMING 2015年第Part3期111卷 395-425页

作者： Gaboardi, Marco Pechoux, Romain Harvard Univ Cambridge MA 02138 USA Univ Dundee Dundee DD1 4HN Scotland Univ Lorraine INRIA Project Carte Loria UMR 7503 Nancy France

Interpretation methods are important tools in implicit computational complexity. They have been proved particularly useful to statically analyze and to limit the complexity of programs. However, most of these studies have been so far applied in the context of term rewriting systems over finite data. In this paper, we show how interpretations can also be used to study properties of lazy first-order functional programs over streams. In particular, we provide some interpretation criteria useful to ensure two kinds of stream properties: space upper bounds and input/output upper bounds. Our space upper bounds criteria ensure global and local upper bounds on the size of each output stream element expressed in terms of the maximal size of the input stream elements. The input/output upper bounds criteria consider instead the relations between the number of elements read from the input stream and the number of elements produced on the output stream. This contribution can be seen as a first step in the development of a methodology aiming at using interpretation properties to ensure space safety properties of programs working on streams. (C) 2015 Elsevier BM. All rights reserved.

关键词： Stream programs Interpretations Program space usage Lazy languages implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

Polynomial time in untyped elementary linear logic

引用

THEORETICAL COMPUTER SCIENCE 2020年 813卷 117-142页

作者： Laurent, Olivier Univ Lyon UCBL CNRS EnslLIP F-69342 Lyon 07 France

We show how to represent polynomial time computation in an untyped version of proof-nets for elementary linear logic. This follows previous work by P. Baillot but which was developed in a typed and affine setting. We ... 详细信息

关键词： implicit computational complexity Polynomial time computation Elementary linear logic Proof nets Strong normalization

来源：评论

学校读者我要写书评

暂无评论

Light logics and optimal reduction: Completeness and complexity

引用

INFORMATION AND COMPUTATION 2011年第2期209卷 118-142页

作者： Baillot, Patrick Coppola, Paolo Dal Lago, Ugo Univ Lyon ENS Lyon LIP UMR CNRS ENSL INRIA UCBL 5668 F-69364 Lyon 07 France Univ Udine Dipartimento Matemat & Informat I-33100 Udine Italy Univ Bologna Dipartimento Sci Informaz I-40127 Bologna Italy Univ Paris 13 F-93430 Villetaneuse France Univ Paris 07 F-75221 Paris 05 France

Typing of lambda-terms in elementary and light affine logic (EAL and LAL, respectively) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, respectively) proof-nets admits a guaranteed polynomial (elementary, respectively) bound: on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping's algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL, respectively) typed terms, Lamping's abstract algorithm also admits a polynomial (elementary, respectively) bound. We also give a proof of its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics). (C) 2010 Elsevier Inc. All rights reserved.

关键词： Lambda calculus Linear logic Optimal reduction implicit computational complexity Proof-nets Light linear logic

来源：评论

学校读者我要写书评

暂无评论

Light types for polynomial time computation in lambda calculus

引用

INFORMATION AND COMPUTATION 2009年第1期207卷 41-62页

作者： Baillot, Patrick Terui, Kazushige Univ Paris 13 CNRS UMR 7030 LIPN F-93430 Villetaneuse France Kyoto Univ Math Sci Res Inst Kyoto 6068501 Japan

We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL. (c) 2008 Elsevier Inc. All rights reserved.

关键词： Linear logic Light linear logic Lambda calculus Type system implicit computational complexity Polynomial time complexity

来源：评论

学校读者我要写书评

暂无评论

On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy

引用

INFORMATION AND COMPUTATION 2015年 241卷 3-31页

作者： Baillot, Patrick Univ Lyon LIP CNRS ENS LyonInriaUCBL Lyon France

Elementary linear logic is a simple variant of linear logic due to Girard and which characterizes in the proofs-as-programs approach the class of elementary functions, that is to say functions computable in time bounded by a tower of exponentials of fixed height. Other systems like light and soft linear logics have then been defined to characterize in a similar way the more interesting complexity class of polynomial time functions, but at the price of either a more complicated syntax or of more sophisticated encodings. These logical systems can serve as the basis of type systems for lambda-calculus ensuring polynomial time complexity bounds on well-typed terms. This paper aims at reviving interest in elementary linear logic by showing that, despite its simplicity, it can capture smaller complexity classes than that of elementary functions. For that we carry a detailed analysis of its normalization procedure, and study the complexity of functions represented by a given type. We then show that by considering a slight variant of this system, with type fixpoints and free weakening (elementary affine logic with fixpoints) we can characterize the complexity of functions of type !W !Bk+2, where Wand Bare respectively types for binary words and booleans. The key point is a sharper study of the normalization bounds. We characterize in this way the class P of polynomial time predicates, and more generally the hierarchy of classes k-EXP, for k >= 0, where k-EXP is the union of DTIME(2(k)(ni)), for i >= 1. (C) 2014 Elsevier Inc. All rights reserved.

关键词： implicit computational complexity Linear logic Lambda-calculus Polynomial time complexity Type systems

来源：评论

学校读者我要写书评

暂无评论

An abstract approach to stratification in linear logic

引用

INFORMATION AND COMPUTATION 2015年 241卷 32-61页

作者： Boudes, Pierre Mazza, Damiano de Falco, Lorenzo Tortora Univ Paris 13 CNRS LIPN Sorbonne Paris Cite F-93430 Villetaneuse France Univ Paris 13 CNRS UMR 7030 LIPNSorbonne Paris Cite F-93430 Villetaneuse France Univ Roma Tre Dipartimento Filosofia Rome Italy

We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cut-elimination procedure (the so-called "light" subsystems), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a general categorical construction applicable to all models of linear logic. We thus learn that stratification may be formulated independently of exponential modalities;when it is forced to be connected to exponential modalities, it yields interesting complexity properties. In particular, from our analysis stem three alternative reformulations of Baillot and Mazza's linear logic by levels: one geometric, one interactive, and one semantic. (C) 2014 Elsevier Inc. All rights reserved.

关键词： implicit computational complexity Light linear logics Denotational semantics Categorical semantics

来源：评论

学校读者我要写书评

暂无评论

Primitive recursion in the abstract

引用

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE 2020年第1期30卷 33-43页

作者： Leivant, Daniel Marion, Jean-Yves Indiana Univ Bloomington IN 47405 USA Univ Paris Diderot Paris France Univ Lorraine CNRS Lorraine Italy LORIA Lorraine Italy

Recurrence can be used as a function definition schema for any nontrivial free algebra, yielding the same computational complexity in all cases. We show that primitive-recursive computing is in fact independent of free algebras altogether, and can be characterized by a generic programming principle, namely the control of iteration by the depletion of finite components of the underlying structure.

关键词： finite structures implicit computational complexity primitive recursion Program termination program variants structure transformation

来源：评论

学校读者我要写书评

暂无评论

Characterizing polynomial and exponential complexity classes in elementary lambda-calculus

引用

INFORMATION AND COMPUTATION 2018年第Part1期261卷 55-77页

作者： Baillot, Patrick De Benedetti, Erika Della Rocca, Simona Ronchi Univ Lyon Univ Claude Bernard Lyon 1 CNRS ENS LyonLIP UMR5668 F-69342 Lyon 07 France Univ Torino Dipartimento Informat Turin Italy

In this paper an implicit characterization of the complexity classes k-EXPand k-FEXP, for k >= 0, is given, by a type assignment system for a stratified lambda-calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k-EXP is characterized by a hierarchy of types. (C) 2018 Elsevier Inc. All rights reserved.

关键词： implicit computational complexity Linear logic Lambda-calculus

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：