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

43rd acm sigplan International conference on programming language design and implementation (PLDI)

作者： Beutner, Raven Ong, C-H Luke Zaiser, Fabian CISPA Helmholtz Ctr Informat Secur Saarbrucken Germany Univ Oxford Oxford England

ISBN: (纸本)9781450392655

We propose a new method to approximate the posterior distribution of probabilistic programs by means of computing guaranteed bounds. The starting point of our work is an interval-based trace semantics for a recursive, higher-order probabilistic programming language with continuous distributions. Taking the form of (super-/subadditive) measures, these lower/upper bounds are non-stochastic and provably correct: using the semantics, we prove that the actual posterior of a given program is sandwiched between the lower and upper bounds (soundness);moreover, the bounds converge to the posterior (completeness). As a practical and sound approximation, we introduce a weight-aware interval type system, which automatically infers interval bounds on not just the return value but also the weight of program executions, simultaneously. We have built a tool implementation, called GuBPI, which automatically computes these posterior lower/upper bounds. Our evaluation on examples from the literature shows that the bounds are useful, and can even be used to recognise wrong outputs from stochastic posterior inference procedures.

关键词： probabilistic programming Bayesian inference verification abstract interpretation operational semantics interval arithmetic type system symbolic execution

来源：评论

学校读者我要写书评

暂无评论

IRDL: An IR Definition language for SSA Compilers 2022

IRDL: An IR Definition Language for SSA Compilers

引用

43rd acm sigplan International conference on programming language design and implementation (PLDI)

作者： Fehr, Mathieu Niu, Jeff Riddle, River Amini, Mehdi Su, Zhendong Grosser, Tobias Univ Edinburgh Edinburgh Midlothian Scotland Univ Waterloo Waterloo ON Canada Modular AI Seattle WA USA Google Mountain View CA USA Swiss Fed Inst Technol Zurich Switzerland

ISBN: (纸本)9781450392655

designing compiler intermediate representations (IRs) is often a manual process that makes exploration and innovation in this space costly. Developers typically use general-purpose programming languages to design IRs. As a result, IR implementations are verbose, manual modifications are expensive, and designing tooling for the inspection or generation of IRs is impractical. While compilers relied historically on a few slowly evolving IRs, domain-specific optimizations and specialized hardware motivate compilers to use and evolve many IRs. We facilitate the implementation of SSA-based IRs by introducing IRDL, a domain-specific language to define IRs. We analyze all 28 domain-specific IRs developed as part of LLVM's MLIR project over the last two years and demonstrate how to express these IRs exclusively in IRDL while only rarely falling back to IRDL's support for generic C++ extensions. By enabling the concise and explicit specification of IRs, we provide foundations for developing effective tooling to automate the compiler construction process.

关键词： Compilers Intermediate Representation MLIR

来源：评论

学校读者我要写书评

暂无评论

Gen: A General-Purpose Probabilistic programming System with Programmable Inference 2019

Gen: A General-Purpose Probabilistic Programming System with...

引用

40th acm sigplan conference on programming language design and implementation (PLDI) part of acm's Federated Computing Research conference (FCRC)

作者： Cusumano-Towner, Marco F. Saad, Feras A. Lew, Alexander K. Mansinghka, Vikash K. MIT Cambridge MA 02139 USA

ISBN: (纸本)9781450367127

Although probabilistic programming is widely used for some restricted classes of statistical models, existing systems lack the flexibility and efficiency needed for practical use with more challenging models arising in fields like computer vision and robotics. This paper introduces Gen, a generalpurpose probabilistic programming system that achieves modeling flexibility and inference efficiency via several novel language constructs: (i) the generative function interface for encapsulating probabilistic models;(ii) interoperable modeling languages that strike different flexibility/efficiency tradeoffs;(iii) combinators that exploit common patterns of conditional independence;and (iv) an inference library that empowers users to implement efficient inference algorithms at a high level of abstraction. We show that Gen outperforms state-of-the-art probabilistic programming systems, sometimes by multiple orders of magnitude, on diverse problems including object tracking, estimating 3D body pose from a depth image, and inferring the structure of a time series.

关键词： Probabilistic programming Markov chain Monte Carlo sequential Monte Carlo variational inference

来源：评论

学校读者我要写书评

暂无评论

Optimal instruction scheduling using integer programming 00

Optimal instruction scheduling using integer programming

引用

acm sigplan' 00 conference on programming language design and implementation (PLDI)

作者： Wilken, K Liu, J Heffernan, M Univ Calif Davis Dept Elect & Comp Engn Davis CA 95616 USA

ISBN: (纸本)9781581131994

This paper presents a new approach to focal instruction scheduling based on integer programming that produces optimal instruction schedules in a reasonable time, even for very large basic blocks. The new approach first uses a set of graph transformations to simplify the data-dependency graph while preserving the optimality of the final schedule. The simplified graph results in a simplified integer program which can be solved much faster. A new integer-programming formulation is then applied to the simplified graph. Various techniques are used to simplify the formulation, resulting in fewer integer-program variables, fever integer-program constraints and fewer terms in some of the remaining constraints, thus reducing integer-program solution time. The new formulation also uses certain adaptively added constraints (cuts) to reduce solution time. The proposed optimal instruction scheduler is built within the Gnu Compiler Collection (GCC) and is evaluated experimentally using the SPEC95 floating point benchmarks. Although optimal scheduling for the target processor is considered intractable, all of the benchmarks' basic blocks are optimally scheduled, including blocks with up to 1000 instructions, while total compile time increases by only 14%.

关键词： Program compilers

来源：评论

学校读者我要写书评

暂无评论

Supporting array programming in X10 1

Supporting array programming in X10

引用

1st acm sigplan International Workshop on Libraries, languages and Compilers for Array programming, ARRAY 2014 - Part of PLDI 2014

作者： Grove, David Milthorpe, Josh Tardieu, Olivier IBM Research Australia Australian National University Australia

ISBN: (纸本)9781450329378

Effective support for array-based programming has long been one of the central design concerns of the X10 programming language. After significant research and exploration, X10 has adopted an approach based on providing arrays via user definable and extensible class libraries. This paper surveys the range of array abstractions available to the programmer in X10 2.4 and describes the key language features and language implementation techniques necessary to make efficient and productive implementations of these abstractions possible.. Copyright © 2014 acm 978-1-4503-2937-8/14/06. 15.00.

关键词： Abstracting

来源：评论

学校读者我要写书评

暂无评论

Once upon a polymorphic type

Conference Record of the Annual ACM Symposium on Principles ...

引用

conference Record of the Annual acm Symposium on Principles of programming languages 1999年 15-28页

作者： Wansbrough, Keith Jones, Simon Peyton Univ of Cambridge Cambridge United Kingdom

We present a sound type-based `usage analysis' for a realistic lazy functional language. Accurate information on the usage of program subexpressions in a lazy functional language permits a compiler to perform a number of useful optimizations. However, existing analyses are either ad-hoc and approximate, or defined over restricted languages. Our work extends the Once Upon A Type system of Turner, Mossin, and Wadler (FPCA'95). Firstly, we add type polymorphism, an essential feature of typed functional programming languages. Secondly, we include general Haskell-style user-defined algebraic data types. Thirdly, we explain and solve the `poisoning problem', which causes the earlier analysis to yield poor results. Interesting design choices turn up in each of these areas. Our analysis is sound with respect to a Launchbury-style operational semantics, and it is straightforward to implement. Good results have been obtained from a prototype implementation, and we are currently integrating the system into the Glasgow Haskell Compiler.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Reusable Inline Caching for JavaScript Performance 2019

Reusable Inline Caching for JavaScript Performance

引用

40th acm sigplan conference on programming language design and implementation (PLDI) part of acm's Federated Computing Research conference (FCRC)

作者： Choi, Jiho Shull, Thomas Torrellas, Josep Univ Illinois Champaign IL 61820 USA

ISBN: (纸本)9781450367127

JavaScript performance is paramount to a user's browsing experience. Browser vendors have gone to great lengths to improve JavaScript's steady-state performance. This has led to sophisticated web applications. However, as users increasingly expect instantaneous page load times, another important goal for JavaScript engines is to attain minimal startup times. In this paper, we reduce the startup time of JavaScript programs by enhancing the reuse of compilation and optimization information across different executions. Specifically, we propose a new scheme to increase the startup performance of Inline Caching (IC), a key optimization for dynamic type systems. The idea is to represent a substantial portion of the IC information in an execution in a context-independent way, and reuse it in subsequent executions. We call our enhanced IC design Reusable Inline Caching (RIC). We integrate RIC into the state-of-the-art Google V8 JavaScript engine and measure its impact on the initialization time of popular JavaScript libraries. By recycling IC information collected from a previous execution, RIC reduces the average initialization time per library by 17%.

关键词： Inline Caching JavaScript Scripting language Dynamic Typing

来源：评论

学校读者我要写书评

暂无评论

Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths

Static Analysis for Probabilistic Programs: Inferring Whole ...

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Sankaranarayanan, Sriram Chakarov, Aleksandar Gulwani, Sumit Univ Colorado Boulder CO 80309 USA Microsoft Res Redmond WA USA

ISBN: (纸本)9781450320146

We propose an approach for the static analysis of probabilistic programs that sense, manipulate, and control based on uncertain data. Examples include programs used in risk analysis, medical decision making and cyber-physical systems. Correctness properties of such programs take the form of queries that seek the probabilities of assertions over program variables. We present a static analysis approach that provides guaranteed interval bounds on the values (assertion probabilities) of such queries. First, we observe that for probabilistic programs, it is possible to conclude facts about the behavior of the entire program by choosing a finite, adequate set of its paths. We provide strategies for choosing such a set of paths and verifying its adequacy. The queries are evaluated over each path by a combination of symbolic execution and probabilistic volume-bound computations. Each path yields interval bounds that can be summed up with a "coverage" bound to yield an interval that encloses the probability of assertion for the program as a whole. We demonstrate promising results on a suite of benchmarks from many different sources including robotic manipulators and medical decision making programs.

关键词： Probabilistic programming Program Verification Volume Bounding Symbolic Execution Monte-Carlo Sampling

来源：评论

学校读者我要写书评

暂无评论

Profile guided code positioning 90

Profile guided code positioning

引用

proceedings of the acm sigplan '90 conference on programming language design and implementation

作者： Pettis, Karl Hansen, Robert C. Hewlett Packard Co California Language Lab Cupertino United States

ISBN: (纸本)0897913647

This paper presents the results of our investigation of code positioning techniques using execution profile data as input into the compilation process. The primary objective of the positioning is to reduce the overhead of the instruction memory hierarchy. After initial investigation in the literature, we decided to implement two prototypes for the Hewlett-Packard Precision Architecture (PA-RISC). The first, built on top of the linker, positions code based on whole procedures. This prototype has the ability to move procedures into an order that is determined by a 'closest is best' strategy. The algorithms we implemented are described through examples in this paper. The performance improvements from our work are also summarized in various tables and charts.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

VeriML: Typed Computation of Logical Terms inside a language with Effects 10

VeriML: Typed Computation of Logical Terms inside a Language...

引用

15th acm sigplan International conference on Functional programming

作者： Stampoulis, Antonis Shao, Zhong Yale Univ Dept Comp Sci New Haven CT 06520 USA

ISBN: (纸本)9781605587943

Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Unfortunately, large scale proof development in these proof assistants is still an extremely difficult and time-consuming task. One major weakness of these proof assistants is the lack of a single language where users can develop complex tactics and decision procedures using a rich programming model and in a typeful manner. This limits the scalability of the proof development process, as users avoid developing domain-specific tactics and decision procedures. In this paper, we present VeriML-a novel language design that couples a type-safe effectful computational language with first-class support for manipulating logical terms such as propositions and proofs. The main idea behind our design is to integrate a rich logical framework-similar to the one supported by Coq-inside a computational language inspired by ML. The language design is such that the added features are orthogonal to the rest of the computational language, and also do not require significant additions to the logic language, so soundness is guaranteed. We have built a prototype implementation of VeriML including both its type-checker and an interpreter. We demonstrate the effectiveness of our design by showing a number of type-safe tactics and decision procedures written in VeriML.

关键词： proof assistants type theory dependent types logical frameworks

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：