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

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Batty, Mark Donaldson, Alastair F. Wickerson, John Univ Kent Canterbury CT2 7NZ Kent England Univ London Imperial Coll Sci Technol & Med London SW7 2AZ England

ISBN: (纸本)9781450335492

Despite the conceptual simplicity of sequential consistency (SC), the semantics of SC atomic operations and fences in the C11 and OpenCL memory models is subtle, leading to convoluted prose descriptions that translate to complex axiomatic formalisations. We conduct an overhaul of SC atomics in C11, reducing the associated axioms in both number and complexity. A consequence of our simplification is that the SC operations in an execution no longer need to be totally ordered. This relaxation enables, for the first time, efficient and exhaustive simulation of litmus tests that use SC atomics. We extend our improved C11 model to obtain the first rigorous memory model formalisation for OpenCL (which extends C11 with support for heterogeneous many-core programming) In the OpenCL setting, we refine the SC axioms still further to give a sensible semantics to SC operations that employ a 'memory scope' to restrict their visibility to specific threads. Our overhaul requires slight strengthenings of both the C11 and the OpenCL memory models, causing some behaviours to become disallowed. We argue that these strengthenings are natural, and that all of the formalised C11 and OpenCL compilation schemes of which we are aware (Power and x86 CPUs for C11, AMD GPUs for OpenCL) remain valid in our revised models. Using the HERD memory model simulator, we show that our overhaul leads to an exponential improvement in simulation time for C11 litmus tests compared with the original model, making exhaustive simulation competitive, time-wise, with the non-exhaustive CDSChecker tool.

关键词： Formal methods graphics processing unit (GPU) heterogeneous programming HOL theorem prover language design program simulation weak memory models

来源：评论

学校读者我要写书评

暂无评论

Newtonian Program Analysis via Tensor Product 16

Newtonian Program Analysis via Tensor Product

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Reps, Thomas Turetsky, Emma Prabhu, Prathmesh Univ Wisconsin Madison WI USA GrammaTech Inc Ithaca NY USA Google Inc Mountain View CA USA

ISBN: (纸本)9781450335492

Recently, Esparza et al. generalized Newton's method a numerical-analysis algorithm for finding roots of real-valued functions to a method for finding fixed-points of systems of equations over semirings. Their method provides a new way to solve interprocedural dataflow-analysis problems. As in its real-valued counterpart, each iteration of their method solves a simpler "linearized" problem. One of the reasons this advance is exciting is that some numerical analysts have claimed that all' effective and fast iterative [numerical] methods are forms (perhaps very disguised) of Newton's method." However, there is an important difference between the dataflow-analysis and numerical-analysis contexts: when Newton's method is used on numerical-analysis problems, multiplicative commutativity is relied on to rearrange expressions of the form "c * X + X * d" into "(c+d) * X." Such equations correspond to path problems described by regular languages. In contrast, when Newton's method is used for interprocedural dataflow analysis, the "multiplication" operation involves function composition, and hence is non-commutative: "c * X + X * d" cannot be rearranged into "(c+d) * X" Such equations correspond to path problems described by linear context-free languages (LCFLs). In this paper, we present an improved technique for solving the LCFL sub-problems produced during successive rounds of New ton's method. Our method applies to predicate abstraction, on which most of today's software model checkers rely.

关键词： Algorithms languages Theory Verification Newton's method polynomial fixed-point equation interprocedural program analysis semiring regular expression tensor product

来源：评论

学校读者我要写书评

暂无评论

Dependent Types and Multi-monadic Effects in F^☆ 16

Dependent Types and Multi-monadic Effects in F<SUP>☆</SUP>

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Swamy, Nikhil Hritcu, Catalin Keller, Chantal Rastogi, Aseem Delignat-Lavaud, Antoine Forest, Simon Bhargavan, Karthikeyan Fournet, Cedric Strub, Pierre-Yves Kohlweiss, Markulf Zinzindohoue, Jean-Karim Zanella-Beguelin, Santiago Microsoft Res Bangalore Karnataka India Inria Rennes France MSR Inria Rennes France UMD Rennes France ENS Paris Paris France IMDEA Software Inst Paris France

ISBN: (纸本)9781450335492

We present a new, completely redesigned, version of F-star, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language. In support of these complementary roles, F-star is a dependently typed, higher-order, call-by-value language with primitive effects including state, exceptions, divergence and IO. Although primitive, programmers choose the granularity at which to specify effects by equipping each effect with a monadic, predicate transformer semantics. F-star uses this to efficiently compute weakest preconditions and discharges the resulting proof obligations using a combination of SMT solving and manual proofs. Isolated from the effects, the core of F-star is a language of pure functions used to write specifications and proof terms its consistency is maintained by a semantic termination check based on a well-founded order. We evaluate our design on more than 55,000 lines of F-star we have authored in the last year, focusing on three main case studies. Showcasing its use as a general-purpose programming language, F-star is programmed (but not verified) in F-star, and bootstraps in both OCaml and F#. Our experience confirms F-star's pay-as-you-go cost model: writing idiomatic ML-like code with no finer specifications imposes no user burden. As a verification-oriented language, our most significant evaluation of F-star is in verifying several key modules in an implementation of the TLS-1.2 protocol standard. For the modules we considered, we are able to prove more properties, with fewer annotations using F-star than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss our use of F-star in mechanizing the metatheory of a range of lambda calculi, starting from the simply typed lambda calculus to System F-omega and even mu F-star, a sizeable fragment of F-star itself these proofs make essential use of F-star's flexible combination of SMT automation and constructiv

关键词： verification proof assistants effectful programming

来源：评论

学校读者我要写书评

暂无评论

programming the World of Uncertain Things (Keynote)

引用

acm SIGPLAN NOTICES 2016年第1期51卷 1-2页

作者： McKinley, Kathryn S. Microsoft Res Redmond WA USA

Computing has entered the era of uncertain data, in which hardware and software generate and reason about estimates. Applications use estimates from sensors, machine learning, big data, humans, and approximate hardware and software. Unfortunately, developers face pervasive correctness, programmability, and optimization problems due to estimates. Most programming languages unfortunately make these problems worse. We propose a new programming abstraction called Uncertain < T > embedded into languages, such as C#, C++, Java, Python, and JavaScript. Applications that consume estimates use familiar discrete operations for their estimates;overloaded conditional operators specify hypothesis tests and applications use them control false positives and negatives;and new compositional operators express domain knowledge. By carefully restricting the expressiveness, the runtime automatically implements correct statistical reasoning at conditionals, relieving developers of the need to implement or deeply understand statistics. We demonstrate substantial programmability, correctness, and efficiency benefits of this programming model for GPS sensor navigation, approximate computing, machine learning, and xBox.

关键词： languages Verification Measurement programming with estimates Probabilistic programming Bayesian logic Lazy evaluation

来源：评论

学校读者我要写书评

暂无评论

Environmental Bisimulations for Probabilistic Higher-Order languages

引用

acm SIGPLAN NOTICES 2016年第1期51卷 595-607页

作者： Sangiorgi, Davide Vignudelli, Valeria Univ Bologna I-40126 Bologna Italy INRIA Rennes France

Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe's in the proofs of congruence. As representative calculi, call-by-name and call-by-value A calculus, and a (call-by-value) A-calculus extended with references (i.e., a store) are considered. In each case full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as `up-to techniques', are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.

关键词： Theory Environmental Bisimulation Probabilistic Lambda Calculus Contextual Equivalence Imperative languages

来源：评论

学校读者我要写书评

暂无评论

Fabular: Regression Formulas as Probabilistic programming

引用

acm SIGPLAN NOTICES 2016年第1期51卷 271-283页

作者： Borgstrom, Johannes Gordon, Andrew D. Ouyang, Long Russo, Claudio Scibior, Adam Szymczak, Marcin Uppsala Univ S-75105 Uppsala Sweden Microsoft Res Bangalore Karnataka India Univ Edinburgh Edinburgh EH8 9YL Midlothian Scotland Stanford Univ Stanford CA 94305 USA Univ Cambridge Cambridge CB2 1TN England MPI Tubingen Tubingen Germany

Regression formulas are a domain-specific language adopted by several R packages for describing an important and useful class of statistical models: hierarchical linear regressions. Formulas are succinct, expressive, and clearly popular, so are they a useful addition to probabilistic programming languages? And what do they mean? We propose a core calculus of hierarchical linear regression, in which regression coefficients are themselves defined by nested regressions (unlike in R). We explain how our calculus captures the essence of the formula DSL found in R. We describe the design and implementation of Fabular, a version of the Tabular schema-driven probabilistic programming language, enriched with formulas based on our regression calculus. To the best of our knowledge, this is the first formal description of the core ideas of R's formula notation, the first development of a calculus of regression formulas, and the first demonstration of the benefits of composing regression formulas and latent variables in a probabilistic programming language.

关键词： Bayesian inference linear regression probabilistic programming relational data hierarchical models

来源：评论

学校读者我要写书评

暂无评论

The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems

引用

acm SIGPLAN NOTICES 2016年第1期51卷 443-455页

作者： Cimini, Matteo Siek, Jeremy G. Indiana Univ Bloomington IN 47405 USA

Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.

关键词： languages Theory gradual typing type systems semantics methodology

来源：评论

学校读者我要写书评

暂无评论

Principal Type Inference for GADTs

引用

acm SIGPLAN NOTICES 2016年第1期51卷 416-428页

作者： Chen, Sheng Erwig, Martin UL Lafayette CACS W Lafayette IN USA Oregon State Univ Corvallis OR 97331 USA

We present a new method for GADT type inference that improves the precision of previous approaches. In particular, our approach accepts more type-correct programs than previous approaches when they do not employ type annotations. A side benefit of our approach is that it can detect a wide range of runtime errors that are missed by previous approaches. Our method is based on the idea to represent type refinements in pattern-matching branches by choice types, which facilitate a separation of the typing and reconciliation phases and thus support case expressions. This idea is formalized in a type system, which is both sound and a conservative extension of the classical Hindley-Milner system. We present the results of an empirical evaluation that compares our algorithm with previous approaches.

关键词： languages Theory Type Inference GADT Choice Type Variational Unification Type Reconciliation

来源：评论

学校读者我要写书评

暂无评论

Breaking through the Normalization Barrier: A Self-Interpreter for F-omega

引用

acm SIGPLAN NOTICES 2016年第1期51卷 5-17页

作者： Brown, Matt Palsberg, Jens Univ Calif Los Angeles Los Angeles CA USA

According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a self-interpreter for System F-omega, a strongly normalizing lambda-calculus. After a careful analysis of the classical theorem, we show that static type checking in F-omega can exclude the proof's diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in F-omega, including a continuation-passing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.

关键词： languages Theory Lambda Calculus Self Representation Self Interpretation Meta programming

来源：评论

学校读者我要写书评

暂无评论

Transforming Spreadsheet Data Types using Examples

引用

acm SIGPLAN NOTICES 2016年第1期51卷 343-356页

作者： Singh, Rishabh Gulwani, Sumit Microsoft Res Redmond WA USA

Cleaning spreadsheet data types is a common problem faced by millions of spreadsheet users. Data types such as date, time, name, and units are ubiquitous in spreadsheets, and cleaning transformations on these data types involve parsing and pretty printing their string representations. This presents many challenges to users because cleaning such data requires some background knowledge about the data itself and moreover this data is typically non-uniform, unstructured, and ambiguous. Spreadsheet systems and programming languages provide some UI-based and programmatic solutions for this problem but they are either insufficient for the user's needs or are beyond their expertise. In this paper, we present a programming by example methodology of cleaning data types that learns the desired transformation from a few input-output examples. We propose a domain specific language with probabilistic semantics that is parameterized with declarative data type definitions. The probabilistic semantics is based on three key aspects: (i) approximate predicate matching, (ii) joint learning of data type interpretation, and (iii) weighted branches. This probabilistic semantics enables the language to handle non-uniform, unstructured, and ambiguous data. We then present a synthesis algorithm that learns the desired program in this language from a set of input-output examples. We have implemented our algorithm as an Excel add-in and present its successful evaluation on 55 benchmark problems obtained from online help forums and Excel product team.

关键词： Algorithms Human Factor Program Synthesis Probabilistic Synthesis Spreadsheet programming programming By Examples Noisy Examples

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：