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

proceedings of the acm sigplan 2002 conference on programming language design and implementation (PLDI'02)

作者： Baker, Jason Hsieh, Wilson C. University of Utah Salt Lake City UT United States

ISBN: (纸本)9781581134636

We have designed and implemented Maya, a vers ion of Java that allows programmers to extend and reinterpret its syntax. Maya generalizes macro systems by treating grammar productions as generic functions, and semantic actions on productions as multimethods on the corresponding generic functions. Programmers can write new generic functions (i.e., grammar productions) and new multimethods (i.e., semantic actions), through which they can extend the grammar of the language and change the semantics of its syntactic constructs, respectively. Maya's multimethods are compile-time metaprograms that transform abstract syntax: they execute at program compile-time, because they are semantic actions executed by the parser. Maya's multimethods can be dispatched on the syntactic structure of the input, as well as the static, source-level types of expressions in the input. In this paper we describe what Maya can do and how it works. We describe how its novel parsing techniques work and how Maya can statically detect certain kinds of errors, such as code that generates references to free variables. Finally, to demonstrate Maya's expressiveness, we describe how Maya can be used to implement the Multi Java language, which was described by Clifton et al. at OOPSLA 2000.

关键词： Java programming language

来源：评论

学校读者我要写书评

暂无评论

A type directed translation of MLF to system F

A type directed translation of MLF to system F

引用

12th acm sigplan International conference on Functional programming

作者： Leijen, Daan Microsoft Research

ISBN: (纸本)9781595938152

The MLF type system by Le Botlan and Remy (2003) is a natural extension of Hindley-Milner type inference that supports full first-class polymorphism, where types can be of higher-rank and impredicatively instantiated. Even though MLF is theoretically very attractive, it has not seen widespread adoption. We believe that this partly because it is unclear how the rich language of MLF types relate to standard System F types. In this article we give the first type directed translation of MLF terms to System F terms. Based on insight gained from this translation, we also define "Rigid MLF" (MLF=), a restriction of MLF where all bound values have a System F type. The expressiveness of MLF= is the same as that of boxy types, but MLF= needs fewer annotations and we give a detailed comparison between them.

关键词： languages design theory first-class polymorphism system F MLF

来源：评论

学校读者我要写书评

暂无评论

Compiling KB-Sized Machine Learning Models to Tiny IoT Devices 2019

Compiling KB-Sized Machine Learning Models to Tiny IoT Devic...

引用

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

作者： Gopinath, Sridhar Ghanathe, Nikhil Seshadri, Vivek Sharma, Rahul Microsoft Res Bengaluru India

ISBN: (纸本)9781450367127

Recent advances in machine learning (ML) have produced KiloByte-size models that can directly run on constrained IoT devices. This approach avoids expensive communication between IoT devices and the cloud, thereby enabling energy-efficient real-time analytics. However, ML models are expressed typically in floating-point, and IoT hardware typically does not support floating-point. Therefore, running these models on IoT devices requires simulating IEEE-754 floating-point using software, which is very inefficient. We present SeeDot, a domain-specific language to express ML inference algorithms and a compiler that compiles SeeDot programs to fixed-point code that can efficiently run on constrained IoT devices. We propose 1) a novel compilation strategy that reduces the search space for some key parameters used in the fixed-point code, and 2) new efficient implementations of expensive operations. SeeDot compiles state-of-the-art KB-sized models to various microcontrollers and low-end FPGAs. We show that SeeDot outperforms 1) software emulation of floating-point (Arduino), 2) high-bitwidth fixed-point (MATLAB), 3) post-training quantization (TensorFlow-Lite), and 4) floating- and fixed-point FPGA implementations generated using high-level synthesis tools.

关键词： Machine Learning IoT device programming language Compiler Fixed-point Microcontroller FPGA

来源：评论

学校读者我要写书评

暂无评论

Perl 6: Reconciling the Irreconcilable 07

Perl 6: Reconciling the Irreconcilable

引用

34th acm sigplan-SIGACT Symposium on Principles of programming languages

作者： Tang, Audrey Pugscode Org Taipei Taiwan

ISBN: (纸本)9781595935755

Perl is a general-purpose language, known for its vast number of freely available libraries. The Perl 6 project was started to improve the language's support for multi-paradigmatic programming, while retaining compatibility with the existing code base. This talk discusses how Perl 6 attempts to reconcile various competing paradigms in the field of programming language design, such as static vs. dynamic typechecking, nominal vs. structural subtyping, prototype vs. class-based objects, and lazy vs. eager evaluation. Moreover, this talk also covers the design and development of Pugs, a self-hosting Perl 6 implementation bootstrapped from Haskell, targeting multiple runtime environments, including Perl 5, JavaScript and Parrot.

关键词： design Experimentation Human factors languages Reliability

来源：评论

学校读者我要写书评

暂无评论

Adding delimited and composable control to a production programming environment

Adding delimited and composable control to a production prog...

引用

12th acm sigplan International conference on Functional programming

作者： Flatt, Matthew Yu, Gang Findler, Robert Bruce Felleisen, Matthias Univ Utah Salt Lake City UT 84112 USA Chinese Acad Sci Inst Software Beijing 100864 Peoples R China Univ Chicago Chicago IL 60637 USA Northeastern Univ Boston MA 02115 USA

ISBN: (纸本)9781595938152

Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programming language research. Numerous papers explain their advantages, how the operators explain each other (or don't), and other aspects of the operators' existence. Production programming languages, however, do not support these operators, partly because their relationship to existing and demonstrably useful constructs-such as exceptions and dynamic binding-remains relatively unexplored. In this paper, we report on our effort of translating the theory of delimited and composable control into a viable implementation for a production system. The report shows how this effort involved a substantial design element, including work with a formal model, as well as significant practical exploration and engineering. The resulting version of PLT Scheme incorporates the expressive combination of delimited and composable control alongside dynamic-wind, dynamic binding, and exception handling. None of the additional operators subvert the intended benefits of existing control operators, so that programmers can freely mix and match control operators.

关键词： design languages

来源：评论

学校读者我要写书评

暂无评论

Study of dead data members in C++ applications

Study of dead data members in C++ applications

引用

proceedings of the 1998 Annual acm sigplan conference on programming language design and implementation, PLDI

作者： Sweeney, Peter P. Tip, Frank IBM Thomas J. Watson Research Cent Yorktown Heights United States

Object-oriented applications may contain data members that can be removed from the application without affecting program behavior. Such `dead' data members may occur due to unused functionality in class libraries, or due to the programmer losing track of member usage as the application changes over time. We present a simple and efficient algorithm for detecting dead data members in C++ applications. This algorithm has been implemented using a prototype version of the IBM VisualAge C++ compiler, and applied to a number of realistic benchmark programs ranging from 600 to 58,000 lines of code. For the non-trivial benchmarks, we found that up to 27.3% of the data members in the benchmarks are dead (average 12.5%), and that up to 11.6% of the object space of these applications may be occupied by dead data members at run-time (average 4.4%).

关键词： C (programming language)

来源：评论

学校读者我要写书评

暂无评论

Fault-tolerant typed assembly language 07

Fault-tolerant typed assembly language

引用

conference on programming language design and implementation

作者： Perry, Frances Mackey, Lester Reis, George A. Ligatti, Jay August, David I. Walker, David Princeton Univ Dept Comp Sci & Elect Engn Princeton NJ 08544 USA Univ S Florida Dept Comp Sci & Comp Engn Tampa FL 33620 USA

ISBN: (纸本)9781595936332

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. Although transient faults do not permanently damage the hardware, they may corrupt computations by altering stored values and signal transfers. In this paper, we propose a new scheme for provably safe and reliable computing in the presence of transient hardware faults. In our scheme, software computations are replicated to provide redundancy while special instructions compare the independently computed results to detect errors before writing critical data. In stark contrast to any previous efforts in this area, we have analyzed our fault tolerance scheme from a formal, theoretical perspective. To be specific, first, we provide an operational semantics for our assembly language, which includes a precise formal definition of our fault model. Second, we develop an assembly-level type system designed to detect reliability problems in compiled code. Third, we provide a formal specification for program fault tolerance under the given fault model and prove that all well-typed programs are indeed fault tolerant. In addition to the formal analysis, we evaluate our detection scheme and show that it only takes 34% longer to execute than the unreliable version.

关键词： languages reliability theory verification transient hardware faults soft faults fault tolerance type systems typed assembly language

来源：评论

学校读者我要写书评

暂无评论

Communication optimizations for parallel C programs 98

Communication optimizations for parallel C programs

引用

proceedings of the 1998 Annual acm sigplan conference on programming language design and implementation, PLDI

作者： Zhu, Yingchun Hendren, Laurie J. McGill Univ Montreal Que Canada

ISBN: (纸本)9780897919876

This paper presents algorithms for reducing the communication overhead for parallel C programs that use dynamically-allocated data structures. The framework consists of an analysis phase called possible-placement analysis, and a transformation phase called communication selection. The fundamental idea of possible-placement analysis is to find all possible points for insertion of remote memory operations. Remote reads are propagated upwards, whereas remote writes are propagated downwards. Based on the results of the possible-placement analysis, the communication selection transformation selects the `best' place for inserting the communication, and determines if pipelining or blocking of communication should be performed. The framework has been implemented in the EARTH-McCAT optimizing/parallelizing C compiler, and experimental results are presented for five pointer-intensive benchmarks running on the EARTH-MANNA distributed-memory parallel architecture. These experiments show that the communication optimization can provide performance improvements of up to 16% over the unoptimized benchmarks.

关键词： C (programming language)

来源：评论

学校读者我要写书评

暂无评论

A Verified Compiler for a Functional Tensor language

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 320-342页

作者： Liu, Amanda Bernstein, Gilbert Chlipala, Adam Ragan-Kelley, Jonathan MIT 77 Massachusetts Ave Cambridge MA 02139 USA Univ Washington Seattle WA 98195 USA

Producing efficient array code is crucial in high-performance domains like image processing and machine learning. It requires the ability to control factors like compute intensity and locality by reordering computations into different stages and granularities with respect to where they are stored. However, traditional pure, functional tensor languages struggle to do so. In a previous publication, we introduced ATL as a pure, functional tensor language capable of systematically decoupling compute and storage order via a set of high-level combinators known as reshape operators. Reshape operators are a unique functional-programming construct since they manipulate storage location in the generated code by modifying the indices that appear on the left-hand sides of storage expressions. We present a formal correctness proof for an implementation of the compilation algorithm, marking the first verification of a lowering algorithm targeting imperative loop nests from a source functional language that enables separate control of compute and storage ordering. One of the core difficulties of this proof required properly formulating the complex invariants to ensure that these storage-index remappings were well-formed. Notably, this exercise revealed a soundness bug in the original published compilation algorithm regarding the truncation reshape operators. Our fix is a new type system that captures safety conditions that were previously implicit and enables us to prove compiler correctness for well-typed source programs. We evaluate this type system and compiler implementation on a range of common programs and optimizations, including but not limited to those previously studied to demonstrate performance comparable to established compilers like Halide.

关键词： functional programming array programming formal verification type systems tensors

来源：评论

学校读者我要写书评

暂无评论

TYPE DECLARATIONS AS SUBTYPE CONSTRAINTS IN LOGIC programming 90

TYPE DECLARATIONS AS SUBTYPE CONSTRAINTS IN LOGIC PROGRAMMIN...

引用

1990 CONF OF THE SPECIAL INTEREST GROUP ON programming languageS OF THE ASSOC FOR COMPUTING MACHINERY : programming language design AND implementation

作者： JACOBS, D UNIV SO CALIF LOS ANGELESCA 90089

ISBN: (纸本)9780897913645

This paper presents a type system for logic programs that supports parametric polymorphism and subtypes. This system follows most knowledge representation and object-oriented schemes in that subtyping is name-based, i.e., τ1 is considered to be a subtype of τ2 iff it is declared as such. We take this as a fundamental principle in the sense that type declarations have the form of subtype constraints. Types are assigned meaning by viewing such constraints as Horn clauses that, together with a few basic axioms, define a subtype predicate. This technique provides a (least) model for types and, at the same time, a sound and complete proof system for deriving subtypes. Using this proof system, we define well-typedness conditions which ensure that a logic program/query respects a set of predicate types. We prove that these conditions are consistent in the sense that every atom of every resolvent produced during the execution of a well-typed program is consistent with its type.

关键词： Logic programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：