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

2014 acm International conference on Object-Oriented-programming-Systems-languages-and-Applications (OOPSLA 14)

作者： Mitschke, Ralf Erdweg, Sebastian Koehler, Mirko Mezini, Mira Salvaneschi, Guido Tech Univ Darmstadt Darmstadt Germany Univ Lancaster Lancaster LA1 4YW England

ISBN: (纸本)9781450325851

An incremental computation updates its result based on a change to its input, which is often an order of magnitude faster than a recomputation from scratch. In particular, incrementalization can make expensive computations feasible for settings that require short feedback cycles, such as interactive systems, IDEs, or (soft) real-time systems. This paper presents i3QL, a general-purpose programming language for specifying incremental computations. i3QL provides a declarative SQL-like syntax and is based on incremental versions of operators from relational algebra, enriched with support for general recursion. We integrated i3QL into Scala as a library, which enables programmers to use regular Scala code for non-incremental subcomputations of an i3QL query and to easily integrate incremental computations into larger software projects. To improve performance, i3QL optimizes user-defined queries by applying algebraic laws and partial evaluation. We describe the design and implementation of i3QL and its optimizations, demonstrate its applicability, and evaluate its performance.

关键词： Incremental Computation Scala Reactive programming

来源：评论

学校读者我要写书评

暂无评论

Parameterized types for Java

Parameterized types for Java

引用

The 1997 24th acm sigplan-SIGACT Symposium on Principles of programming languages, POPL'97

作者： Myers, Andrew C. Bank, Joseph A. Liskov, Barbara Massachusetts Inst of Technology Cambridge MA United States

Java offers the real possibility that most programs can be written in a type-safe language. However, for Java to be broadly useful, it needs additional expressive power. This paper extends Java in one area where more power is needed: support for parametric polymorphism, which allows the definition and implementation of generic abstractions. We discuss both the rationale for our design decisions and the impact of the extension on other parts of Java, including arrays and the class library. We also describe optional extensions to the Java virtual machine to allow parameterized bytecodes, and how to verify them efficiently. We have extended the Jave bytecode interpreter to provide good performance for parameterized code in both execution speed and code size, without slowing down non-parameterized code.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Load-reuse analysis: design and evaluation

Proceedings of the ACM SIGPLAN Conference on Programming Lan...

引用

Proceedings of the acm sigplan conference on programming language design and implementation (pldi) 1999年 64-76页

作者： Bodik, Rastislav Gupta, Rajiv Soffa, Mary Lou Univ of Pittsburgh Pittsburgh United States

Load-reuse analysis finds instructions that repeatedly access the same memory location. This location can be promoted to a register, eliminating redundant loads by reusing the results of prior memory accesses. This paper develops a load-reuse analysis and designs a method for evaluating its precision. In designing the analysis, we aspire for completeness - the goal of exposing all reuse that can be harvested by a subsequent program transformation. For register promotion, a suitable transformation is partial redundancy elimination (PRE). To approach the ideal goal of PRE-completeness, the load-reuse analysis is phrased as a data-flow problem on a program representation that is path-sensitive, as it detects reuse even when it originates in a different instruction along each control flow path. Furthermore, the analysis is comprehensive, as it treats scalar, array and pointer-based loads uniformly. In evaluating the analysis, we compare it with an ideal analysis. By observing the run-time stream of memory references, we collect all PRE-exploitable reuse and treat it as the ideal analysis performance. To compare the (static) load-reuse analysis with the (dynamic) ideal reuse, we use an estimator algorithm that computes, given a data-flow solution and a program profile, the dynamic amount of reuse detected by the analysis. We developed a family of estimators that differ in how well they bound the profiling error inherent in the edge profile. By bounding the error, the estimators offer a precise and practical method for determining the run-time optimization benefit. Our experiments show that about 55% of loads executed in Spec95 exhibit reuse. Of those, our analysis exposes about 80%.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

conferences with improved management and style

Conferences with improved management and style

引用

作者： Wadler, Philip Department of Theoretical Computer Science University of Edinburgh Royal Society of Edinburgh

sigplan sponsors the premier conferences in the area of programming language research and maintains a vigorous program of workshops. sigplan explores programming language concepts and tools focusing on design, implementation and efficient use. It has two types of relationships with conferences and workshops, sponsorship and in-cooperation. It also promotes a Republication Policy to clarify issues of overlap between related publications. It has arranged bulk provisions of conference management services from Softconf, which uses START V2. The service includes web hosting which relieves conference organizers of the responsibility for running the web server. The bulk rate negotiated with Softconf reduces cost to sigplan while at the same time improves the level of services.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Opus: A Smalltalk production system 87

Opus: A Smalltalk production system

引用

1987 conference on Object Oriented programming Systems languages and Applications, OOPSLA 1987

作者： Laursen, Jane Atkinson, Robert System Concepts Laboratory Xerox Palo Alto Research Center United States

ISBN: (纸本)0897912470

Opus is a tool for rule-based programming which integrates a production system paradigm with the Smalltalk-80 environment. Opus currently provides a data-driven production system that allows the programmer considerable freedom, including access to the full functionality of the Smalltalk-80 language, and the ability to match rules with arbitrary objects in the environment. We present the goals for the design, a description of the system and its implementation, and discuss issues raised by this approach. © 1987 acm.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Effective Interactive Proofs for Higher-Order Imperative Programs

Effective Interactive Proofs for Higher-Order Imperative Pro...

引用

14th acm sigplan International conference on Functional programming

作者： Chlipala, Adam Malecha, Gregory Morrisett, Greg Shinnar, Avraham Wisnesky, Ryan Harvard Univ Cambridge MA 02138 USA

ISBN: (纸本)9781605583327

We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules. We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted;namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.

关键词： functional programming interactive proof assistants dependent types separation logic

来源：评论

学校读者我要写书评

暂无评论

Communicating reactive processes 93

Communicating reactive processes

引用

20th Annual acm sigplan-SIGACT Symposium on Principles of programming languages, POPL'93

作者： Berry, G. Ramesh, S. Shyamasundar, R.K. Ecole des Mines Sophia-Antipolis France

ISBN: (纸本)0897915607

We present a new programming paradigm called Communicating Reactive Processes or CRP that unifies the capabilities of asynchronous and synchronous concurrent programming languages. Asynchronous languages such as CSP, OCCAM, or ADA are well-suited for distributed algorithms;their processes are loosely coupled and communication takes time. The ESTEREL synchronous language is dedicated to reactive systems;its processes are tightly coupled and deterministic, communication being realized by instantaneous broadcasting. Complex applications such as process or robot control require to couple both forms of concurrency, which is the object of CRP. A CRP program consists of independent locally reactive ESTEREL nodes that communicate with each other by CSP rendezvous. CRP faithfully extends both ESTEREL and CSP and adds new possibilities such as precise local watchdogs on rendezvous. We present the design of CRP, its semantics, a translation into classical process calculi for program verification, an application example, and implementation issues.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

Dynamic scheduling method for irregular parallel programs

Dynamic scheduling method for irregular parallel programs

引用

acm sigplan '92 conference on programming language design and implementation, pldi 1992

作者： Lucco, Steven UC Berkeley Berkeley CA United States

ISBN: (纸本)0897914759

This paper develops a methodology for compiling and executing irregular parallel programs. Such programs implement parallel operations whose size and work distribution depend on input data. We show a fundamental relationship between three quantities that characterize an irregular parallel computation: the total available parallelism, the optimal grain size, and the statistical variance of execution times for individual tasks. This relationship yields a dynamic scheduling algorithm that substantially reduces the overhead of executing irregular parallel operations. We incorporated this algorithm into an extended Fortran compiler. The compiler accepts as input a subset of Fortran D which includes blocked and cyclic decompositions and perfect alignment;it outputs Fortran 77 augmented with calls to library routines written in C. For irregular parallel operations, the compiled code gathers information about available parallelism and task execution time variance and uses this information to schedule the operation. On distributed memory architectures, the compiler encodes information about data access patterns for the runtime scheduling system so that it can preserve communication locality. We evaluated these compilation techniques using a set of application programs including climate modeling, circuit simulation, and x-ray tomography, that contain irregular parallel operations. The results demonstrate that, for these applications, the dynamic techniques described here achieve near-optimal efficiency on large numbers of processors. In addition, they perform significantly better, on these problems, than any previously proposed static or dynamic scheduling algorithm.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

Using ARM TrustZone to build a Trusted language Runtime for mobile applications 14

Using ARM TrustZone to build a Trusted Language Runtime for ...

引用

19th International conference on Architectural Support for programming languages and Operating Systems, ASPLOS 2014

作者： Santos, Nuno Raj, Himanshu Saroiu, Stefan Wolman, Alec INESC-ID Instituto Superior Técnico University of Lisbon Portugal Microsoft Research Portugal

ISBN: (纸本)9781450323055

paper presents the design, implementation, and evaluation of the Trusted language Runtime (TLR), a system that protects the confidentiality and integrity of .NET mobile applications from OS security breaches. TLR enables separating an application's security-sensitive logic from the rest of the application, and isolates it from the OS and other apps. TLR provides runtime support for the secure component based on a .NET implementation for embedded devices. TLR reduces the TCB of an open source .NET implementation by a factor of 78 with a tolerable performance cost. The main benefit of the TLR is to bring the developer benefits of managed code to trusted computing. With the TLR, developers can build their trusted components with the productivity benefits of modern high-level languages, such as strong typing and garbage collection. Copyright is held by the owner/author(s).

关键词： Trusted computing

来源：评论

学校读者我要写书评

暂无评论

SLE 2016 - Proceedings of the 2016 acm sigplan International conference on Software language Engineering, co-located with SPLASH 2016

SLE 2016 - Proceedings of the 2016 ACM SIGPLAN International...

引用

9th acm sigplan International conference on Software language Engineering, SLE 2016

ISBN: (纸本)9781450344470

The proceedings contain 23 papers. The topics discussed include: parsing and reflective printing, bidirectionally;taming context-sensitive languages with principled stateful parsing;efficient development of consistent projectional editors using grammar cells;experiences of Models@run-time with EMF and CDO;runtime support for rule-based access-control evaluation through model-transformation;object-oriented design pattern for DSL program monitoring;execution framework of the GEMOC studio;language design and implementation for the domain of coding conventions;BSML-mbeddr: integrating semantically configurable state-machine models in a C programming environment;adding uncertainty and units to quantity types in software models;FRaMED: full-fledge role modeling editor;towards a universal code formatter through machine learning;the IDE portability problem and its solution in Monto;principled syntactic code completion using placeholders;automated testing support for reactive domain-specific modelling languages;symbolic execution of high-level transformations;and raincode assembler compiler.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：