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

12th asian symposium on programming languages and systems, aplas 2014

ISBN: (纸本)9783319127354

the proceedings contain 25 papers. the special focus in this conference is on programming languages and systems. the topics include: Optimized compilation of multiset rewriting with comprehensions;automatic memory management based on program transformation using ownership;a formalized proof of strong normalization for guarded recursive types;a flexible language for policies;a method for scalable and precise bug finding using program analysis and model checking;model-checking for android malware detection;resource protection using atomics;resource analysis of complex programs with cost equations;compositional entailment checking for a fragment of separation logic;automatic constrained rewriting induction towards verifying procedural programs;inferring grammatical summaries of string values;profiling java objects without overhead in java heaps;call-by-value in a basic logic for interaction and a precise and abstract memory model for C using symbolic values.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Adaptable Traces for Program Explanations 19th

Adaptable Traces for Program Explanations

引用

19th asian symposium on programming languages and systems (aplas)

作者： Bajaj, Divya Erwig, Martin Fedorin, Danila Gay, Kai Oregon State Univ Corvallis OR 97331 USA

ISBN: (纸本)9783030890513;9783030890506

Program traces are a sound basis for explaining the dynamic behavior of programs. Alas, program traces can grow big very quickly, even for small programs, which diminishes their value as explanations. In this paper we demonstrate how the systematic simplification of traces can yield succinct program explanations. Specifically, we introduce operations for transforming traces that facilitate the abstraction of details. the operations are the basis of a query language for the definition of trace filters that can adapt and simplify traces in a variety of ways. the generation of traces is governed by a variant of Call-By-Value semantics which specifically supports parsimony in trace representations. We show that our semantics is a conservative extension of Call-By-Value that can produce smaller traces and that the evaluation traces preserve the explanatory content of proof trees at a much smaller footprint.

关键词： Semantics Language design Domain-specific languages

来源：评论

学校读者我要写书评

暂无评论

Existential Types for Relaxed Noninterference 17th

Existential Types for Relaxed Noninterference

引用

17th asian symposium on programming languages and systems (aplas)

作者： Cruz, Raimil Tanter, Eric Univ Chile Comp Sci Dept DCC PLEIAD Lab Santiago Chile

ISBN: (纸本)9783030341756;9783030341749

Information-flow security type systems ensure confidentiality by enforcing noninterference: a program cannot leak private data to public channels. However, in practice, programs need to selectively declassify information about private data. Several approaches have provided a notion of relaxed noninterference supporting selective and expressive declassification while retaining a formal security property. the labels-as-functions approach provides relaxed noninterference by means of declassification policies expressed as functions. the labels-as-types approach expresses declassification policies using type abstraction and faceted types, a pair of types representing the secret and public facets of values. the original proposal of labels-as-types is formulated in an object-oriented setting where type abstraction is realized by subtyping. the object-oriented approach however suffers from limitations due to its receiver-centric paradigm. In this work, we consider an alternative approach to labels-as-types, applicable in non-object-oriented languages, which allows us to express advanced declassification policies, such as extrinsic policies, based on a different form of type abstraction: existential types. An existential type exposes abstract types and operations on these;we leverage this abstraction mechanism to express secrets that can be declassified using the provided operations. We formalize the approach in a core functional calculus with existential types, define existential relaxed noninterference, and prove that well-typed programs satisfy this form of type-based relaxed noninterference.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Lightweight Functional Logic Meta-programming 17th

Lightweight Functional Logic Meta-Programming

引用

17th asian symposium on programming languages and systems (aplas)

作者： Amin, Nada Byrd, William E. Rompf, Tiark Harvard Univ Cambridge MA 02138 USA Univ Alabama Birmingham Birmingham AL 35294 USA Purdue Univ W Lafayette IN 47907 USA

ISBN: (纸本)9783030341756;9783030341749

Meta-interpreters in Prolog are a powerful and elegant way to implement language extensions and non-standard semantics. But how can we bring the benefits of Prolog-style meta-interpreters to systems that combine functional and logic programming? In Prolog, a program can access its own structure via reflection, and meta-interpreters are simple to implement because the "pure" core language is small. Can we achieve similar elegance and power for larger systems that combine different paradigms? In this paper, we present a particular kind of functional logic metaprogramming, based on embedding a small first-order logic system in an expressive host language. Embedded logic engines are not new, as exemplified by various systems including miniKanren in Scheme and LogicT in Haskell. However, previous embedded systems generally lack metaprogramming capabilities in the sense of meta-interpretation. Indeed, shallow embeddings usually do not support reflection. Instead of relying on reflection for meta-programming, we show how to adapt popular multi-stage programming techniques to a logic programming setting and use the embedded logic to generate reified firstorder structures, which are again simple to interpret. Our system has an appealing power-to-weight ratio, based on the simple and general notion of dynamically scoped mutable variables. We also show how, in many cases, non-standard semantics can be realized without explicit reification and interpretation, but instead by customizing program execution through the host language. As a key example, we extend our system with a tabling/memoization facility. the need to interact with mutable variables renders this a highly nontrivial challenge, and the crucial insight is to extract symbolic representations of their side effects from memoized rules. We demonstrate that multiple independent semantic modifications can be combined successfully in our system, for example tabling and tracing.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Open Call-by-Value 14th

Open Call-by-Value

引用

14th asian symposium on programming languages and systems (aplas)

作者： Accattoli, Beniamino Guerrieri, Giulio Inria UMR 7161 Ecole Polytech LIX Palaiseau France Aix Marseille Univ CNRS Cent Marseille I2M Marseille France

ISBN: (纸本)9783319479576;9783319479583

the elegant theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required, and it is well known that the operational semantics of call-by-value becomes problematic in this case. Here we study the intermediate setting-that we call Open Call-by-Value-of weak evaluation with open terms, on top of which Gregoire and Leroy designed the abstract machine of Coq. Various calculi for Open Call-by-Value already exist, each one with its pros and cons. this paper presents a detailed comparative study of the operational semantics of four of them, coming from different areas such as the study of abstract machines, denotational semantics, linear logic proof nets, and sequent calculus. We show that these calculi are all equivalent from a termination point of view, justifying the slogan Open Call-by-Value.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

What is the essence of bidirectional programming? 12

What is the essence of bidirectional programming?

引用

12th asian symposium on programming languages and systems, aplas 2014

作者： Hu, Zhenjiang National Institute of Informatics Japan

来源：评论

学校读者我要写书评

暂无评论

Automatic memory management based on program transformation using ownership 12

Automatic memory management based on program transformation ...

引用

12th asian symposium on programming languages and systems, aplas 2014

作者： Sonobe, Tatsuya Suenaga, Kohei Igarashi, Atsushi Kyoto University Kyoto Japan

ISBN: (纸本)9783319127354

We present a type-based program transformation for an imperative programming language with manual memory-management primitives (e.g., malloc and free in C). Our algorithm, given a program with potential memory leaks, inserts memory-deallocating instructions to the program so that the resulting program does not contain memory leaks. We design the algorithm as type reconstruction for an extension of the ownership-based type system by Suenaga and Kobayashi. © Springer International Publishing Switzerland 2014.

关键词： C (programming language)

来源：评论

学校读者我要写书评

暂无评论

Logic programming and logarithmic space 12

Logic programming and logarithmic space

引用

12th asian symposium on programming languages and systems, aplas 2014

作者： Aubert, CléMent Bagnol, Marc Pistone, Paolo Seiller, thomas Aix Marseille Université CNRS Centrale Marseille I2M UMR 7373 Marseille13453 France I.H.É.S Le Bois-Marie 35 Route de Chartres Bures-sur-Yvette91440 France

ISBN: (纸本)9783319127354

We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof *** show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation. © Springer International Publishing Switzerland 2014.

关键词： Logic programming

来源：评论

学校读者我要写书评

暂无评论

Least upper bounds for probability measures and their applications to abstractions

引用

INFORMATION AND COMPUTATION 2014年第0期234卷 68-106页

作者： Chadha, Rohit Viswanathan, Mahesh Viswanathan, Ramesh Univ Illinois Dept Comp Sci Urbana IL 61801 USA Bell Labs Holmdel NJ 07733 USA

Least upper bounds play an important role in defining the semantics of programming languages, and in abstract interpretations. In this paper, we identify conditions on countable ordered measurable spaces that ensure the existence of least upper bounds for all sets of probability measures. these conditions are shown to be necessary as well for any measurable space not satisfying these conditions, there are (finite) sets of probability measures for which no least upper bound exists. For measurable spaces meeting these conditions, the existence of least upper bounds is established constructively. Based on this least upper bound construction, we present a novel abstraction method applicable to Discrete Time Markov Chains (DTMCs), Markov Decision Processes (MDPs), and Continuous Time Markov Chains (CTMCs). the main advantage of the new abstraction techniques is that the resulting abstract models are purely probabilistic that may be more amenable to automated analysis than models with both nondeterministic and probabilistic transitions which arise from previously known abstraction techniques. (C) 2014 Elsevier Inc. All rights reserved.

关键词： programming important probability automatic analysis programming Supremum Upper bound Markov chain programming language semantics Abstraction Tree graphs Measurable space

来源：评论

学校读者我要写书评

暂无评论

A Hierarchical Architecture Description for Flexible Multicore System Simulation 12

A Hierarchical Architecture Description for Flexible Multico...

引用

12th IEEE International symposium on Parallel and Distributed Processing with Applications (ISPA)

作者： Bruckschloegl, thomas Oey, Oliver Rueckauer, Michael Stripf, Timo Becker, Juergen Karlsruhe Inst Technol Inst Informat Proc Technol ITIV D-76021 Karlsruhe Germany

ISBN: (纸本)9781479942930

As processors and systems on chip in the embedded world increasingly become multicore, parallel programming remains a difficult, time-consuming and complicated task. End users who are not parallel programming experts have a need to exploit such processors and architectures, using high level programming languages, like Scilab or MATLAB. the ALMA toolset solves this problem: it takes Scilab code as input and produces parallel code for embedded multiprocessor systems on chip, using platform quasi-agnostic optimizations. the platform information is provided by an architecture description language designed for the purpose of a flexible system description as well as simulation. A hierarchical system description in combination with a parameterizable simulation environment allows fine-grained trade-offs between simulation performance and simulation accuracy.

关键词： Accuracy Multicoreprocessing Optimization Parallelprocessing Programprocessors System-on-chip system-on-chip Architecture description languages PROCESSOR multiprocessor system on chip ARCHITECTURE Multi-core processors systems simulation Parallel programming Simulated Environment Building construction FLEXIBLE

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：