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

Formally Verified Resource Bounds through implicit computational complexity 26

Formally Verified Resource Bounds through Implicit Computati...

ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Companion)

作者： Rusch, Neea Augusta Univ Augusta GA 30912 USA

ISBN: (纸本)9781450399012

Automatic complexity analysis has not reached mainstream adoption due to outstanding challenges, such as scalability and usability, and no formally verified analyzer exists. However, the need to evaluate resource usage is crucial: even a guaranteed correct program, whose memory usage exceeds available resources, is unreliable. The field of implicit computational complexity (ICC) offers a potential avenue to resolving some of these outstanding challenges by introducing unique, machine-independent, and flexible approaches to program analysis. But since ICC techniques are mostly theoretical, it is unclear how strongly these assumptions hold in practice. This project defines a 3-directional plan-focused on practical analysis, compiler-integration, and formal verification-to assess the suitability of ICC to address outstanding challenges in automatic complexity analysis.

关键词： implicit computational complexity Automatic complexity Analysis Program Verification

来源：评论

学校读者我要写书评

暂无评论

Reversible computing and implicit computational complexity

引用

SCIENCE OF COMPUTER PROGRAMMING 2022年 213卷 102723-102723页

作者： Kristiansen, Lars Univ Oslo Dept Informat Oslo Norway Univ Oslo Dept Math Oslo Norway

We argue that there is a link between implicit computational complexity theory and reversible computation. We introduce inherently reversible programming languages which capture the complexity classes ETImE and p. Furthermore, we discuss and analyze higher order versions of our reversible programming languages. (c) 2021 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY license (http://***/licenses/by/4.0/).

关键词： Reversible computing Invertible programming languages implicit computational complexity complexity classes Turing machines

来源：评论

学校读者我要写书评

暂无评论

implicit computational complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

引用

JOURNAL OF AUTOMATED REASONING 2019年第4期63卷 813-855页

作者： Baillot, Patrick Barthe, Gilles Dal Lago, Ugo Univ Lyon CNRS EnsL UCBLLIP F-69342 Lyon 07 France IMDEA Software Inst Madrid Spain Univ Bologna Bologna Italy INRIA Sophia Antipolis France

We define a call-by-value variant of Godel's system T with references, and equip it with a linear dependent type and effect system, called dlT, that can estimate the time complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, in the sense that it over-approximates the complexity of executing the programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of dlT. Finally, we demonstrate the usefulness of dlT for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich-Levin theorem.

关键词： implicit computational complexity complexity analysis Linear dependent types Cryptographic proofs

来源：评论

学校读者我要写书评

暂无评论

Polynomial Time and Dependent Types

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2024年第POPL期8卷 2288-2317页

作者： Atkey, Robert Univ Strathclyde 26 Richmond St Glasgow G1 1XH Lanark Scotland

We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann. Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs' resource usage, and to theoretical use as a form of synthetic computational complexity theory.

关键词： type theory implicit computational complexity linear logic

来源：评论

学校读者我要写书评

暂无评论

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories 32

Enumerating Error Bounded Polytime Algorithms Through Arithm...

引用

32nd EACSL Annual Conference on Computer Science Logic (CSL)

作者： Antonelli, Melissa Dal Lago, Ugo Davoli, Davide Oitavem, Isabel Pistone, Paolo Helsinki Inst Informat Technol Helsinki Finland Bologna Univ Bologna Italy Univ Cote Azur Inria Sophia Antipolis France NOVA FCT Ctr Math & Applicat NOVA Math Caparica Portugal NOVA FCT Dept Math Caparica Portugal

ISBN: (纸本)9783959773102

We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory a la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPPT and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPPT, where T = I Delta(0) + Exp is a well-studied theory based on bounded induction.

关键词： Bounded Arithmetic Randomized Computation implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

implicit recursion-theoretic characterizations of counting classes

引用

ARCHIVE FOR MATHEMATICAL LOGIC 2022年第7-8期61卷 1129-1144页

作者： Dal Lago, Ugo Kahle, Reinhard Oitavem, Isabel Univ Bologna Bologna Italy INRIA Sophia Antipolis Valbonne France Univ Tubingen Carl Friedrich von Weizsacker Ctr Tubingen Germany Univ Nova Lisboa CMA FCT Caparica Portugal Univ Nova Lisboa NOVA Sch Sci & Technol CMA & DM P-2829515 Caparica Portugal

We give recursion-theoretic characterizations of the counting class #P, the class of those functions which count the number of accepting computations of non-deterministic Turing machines working in polynomial time. Moreover, we characterize in a recursion-theoretic manner all the levels {#P-k}(k is an element of N) of the counting hierarchy of functions FCH, which result from allowing queries to functions of the previous level, and FCH itself as a whole. This is done in the style of Bellantoni and Cook's safe recursion, and it places #P in the context of implicit computational complexity. Namely, it relates #P with the implicit characterizations of FPTIME (Bellantoni and Cook, Comput Complex 2:97-110,1992) and FPSPACE (Oitavem, Math Log Q 54(3):317-323, 2008), by exploiting the features of the tree-recursion scheme of FPSPACE.

关键词： #P Counting hierarchy implicit computational complexity Function algebras Recursion-theoretic characterizations

来源：评论

学校读者我要写书评

暂无评论

Types for complexity of Parallel Computation in Pi-Calculus 1

引用

30th European Symposium on Programming (ESOP) Held as Part of the 24th European Joint Conferences on Theory and Practice of Software (ETAPS)

作者： Baillot, Patrick Ghyselen, Alexis Univ Claude Bernard Lyon 1 LIP Univ Lyon CNRSENS Lyon F-69342 Lyon 07 France

ISBN: (数字)9783030720193

ISBN: (纸本)9783030720193;9783030720186

Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular some systems allow to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of the pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions, and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by size types and by input/output types, with additional temporal information about communications.

关键词： Type Systems Pi-calculus Process Calculi complexity Analysis implicit computational complexity Size Types

来源：评论

学校读者我要写书评

暂无评论

Types for complexity of Parallel Computation in Pi-calculus

引用

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 2022年第3期44卷 15-15页

作者： Baillot, Patrick Ghyselen, Alexis Univ Claude Bernard Lyon 1 Univ Lyon LIP ENS LyonCNRS F-69342 Lyon 07 France Univ Lille CRIStAL Bat ESPRITAve Henri Poincare F-59655 Villeneuve Dascq France Univ Bologna Alma Mater Studiorum DIAPASoN Via Zamboni 33 I-40126 Bologna Italy

Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular, some systems allow one to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by sized types and by input/output types, with additional temporal information about communications.

关键词： Type systems pi-calculus process calculi complexity analysis implicit computational complexity sized types

来源：评论

学校读者我要写书评

暂无评论

A TIER-BASED TYPED PROGRAMMING LANGUAGE CHARACTERIZING FEASIBLE FUNCTIONALS

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2022年第1期18卷 33:1-33:31页

作者： Hainry, Emmanuel Kapron, Bruce M. Marion, Jean-Yves Pechoux, Romain Univ Lorraine CNRS INRIA LORIA F-54000 Nancy France Univ Victoria Victoria BC Canada

The class of Basic Feasible Functionals BFF2 is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF2 based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not overly constrain the expressive power of the language.

关键词： Feasible Functionals BFF implicit computational complexity tiering type-2 type system

来源：评论

学校读者我要写书评

暂无评论

Combining linear logic and size types for implicit complexity

引用

THEORETICAL COMPUTER SCIENCE 2020年 813卷 70-99页

作者： Baillot, Patrick Ghyselen, Alexis Univ Claude Bernard Lyon I Univ Lyon CNRS ENS Lyon F-69342 Lyon 07 France

Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its I-modality controlling duplication. An instance of this is light linear logic for polynomial time computation [5]. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. This second approach is illustrated for instance by non-size-increasing types [8]. However, both approaches suffer from limitations. The first one, that of linear logic, has a limited intensional expressivity, that is to say some natural polynomial time programs are not typable. As to the second approach it is essentially linear, more precisely it does not allow for a non-linear use of functional arguments. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. The source language we consider is a lambda-calculus with datatypes and iteration, that is to say a variant of Gtidel's system T. Our goal is to design a system for this language allowing both to handle non-linear functional arguments and to keep a good intensional expressivity. We illustrate our methodology by choosing the system of elementary linear logic (ELL) and combining it with a system of linear size types. We discuss the expressivity of this new type system, called sEAL, and prove that it gives a characterization of the complexity classes FPTIME and 2k-FEXPTIME, for k >= 0. (C) 2019 Elsevier B.V. All rights reserved.

关键词： implicit computational complexity lambda-calculus Linear logic Type systems Polynomial time complexity Size types

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：