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

18th acm sigplan-SIGACT Symposium on Principles of programming languages, POPL 1991

作者： Mitchell, John Meldal, Sigurd Madhav, Neel Dept. of Computer Science Stanford University StanfordCA94305 United States Dept. of Informatics University of Bergen Bergen Norway

ISBN: (纸本)0897914198

We describe a general module language integrating abstract data types, specifications and object-oriented concepts. the framework is based on the Standard ML module system, with three main extensions: subtyping, a form of object derived from ML structures, and inherit ante primitives. the language aims at supporting a range of programming styles, including mixtures of object-oriented programming and programs built around specified algebraic or higher-order abstract data types. We separate specification from implementation, and provide independent inheritance mechanisms for each. In order to support binary operations on objects within this framework, we introduce "internal interfaces" which govern the way that function components of one structure may access components of another. the language design has been tested by writing a number of program examples;an implementation is under development in the context of a larger project. © 1990 acm.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Synthesizing Transformations on Hierarchically Structured Data

引用

acm sigplan NOTICES 2016年第6期51卷 508-521页

作者： Yaghmazadeh, Navid Klinger, Christian Dillig, Isil Chaudhuri, Swarat Univ Texas Austin Austin TX 78712 USA Univ Freiburg Freiburg Germany Rice Univ Houston TX 77251 USA

this paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-driven synthesis algorithm for HDT transformations. Our central insight is to reduce the problem of synthesizing tree transformers to the synthesis of list transformations that are applied to the paths of the tree. the synthesis problem over lists is solved using a new algorithm that combines SMT solving and decision tree learning. We have implemented our technique in a system called HADES and show that HADES can automatically synthesize a variety of interesting transformations collected from online forums.

关键词： languages Program synthesis programming by example data transformations

来源：评论

学校读者我要写书评

暂无评论

Proceedings of the 6th International conference on Functional programming languages and Computer Architecture (FPCA '93)

Proceedings of the 6th International Conference on Functiona...

引用

Proceedings of the 6th International conference on Functional programming languages and Computer Architecture (FPCA '93)

ISBN: (纸本)089791595X

the conference materials contain 33 papers. the topics covered include experience with functional programming applications, theory and implementation of types, storage reclamation, semantics analysis of imperative extensions, compiling and performance evaluation, language design, compiler optimization, static analysis, functional algorithms and partial evaluation.

关键词： Computer simulation languages

来源：评论

学校读者我要写书评

暂无评论

Workflow-based composition of web-services: a business model or a programming paradigm? 6

Workflow-based composition of web-services: a business model...

引用

6th International Enterprise Distributed Object Computing

作者： Ganesarajah, D Lupu, E NDS Orbis London England

ISBN: (纸本)0769517420

While SOAP/XML is perceived as the appropriate interoperability level for web-services, companies compete to provide workflow-based tools for web-service integration. this paper presents the design and implementation of a prototype workflow management system for building new web-services from a workflow of existing web-services. this enables the creation of multiple layers of value-added service providers and provides fast service creation, customisation and deployment. the system caters for multiple workflow paradigms, provides an axtensible language for workflow specification and emphasises encapsulation and tight constraints on workflow execution. To expose a workflow Of web-services as a web-service, several design steps have been required including the deployment as a web-service of the generic workflow engine and a generalisation of the Visitor Pattern to concurrent visitors.

关键词： Web services

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

GPCE 2016 - Proceedings of the 2016 acm sigplan International conference on Generative programming: Concepts and Experiences, co-located with SPLASH 2016

GPCE 2016 - Proceedings of the 2016 ACM SIGPLAN Internationa...

引用

15th acm sigplan International conference on Generative programming: Concepts and Experiences, GPCE 2016

ISBN: (纸本)9781450344463

the proceedings contain 20 papers. the topics discussed include: Recaf: Java dialects as libraries;classless Java;extensible modeling with managed data in Java;actor profiling in virtual execution environments;bootstrapping domain-specific meta-languages in language workbenches;dependence-driven delimited CPS transformation for JavaScript;synthesizing regular expressions from examples for introductory automata assignments;programmable semantic fragments: the design and implementation of typy;delaying decisions in variable concern hierarchies;automatic code generation in practice: experiences with embedded robot controllers;a change-centric approach to compile configurable systems with #ifdefs;a feature-based personalized recommender system for product-line configuration;IncLing: efficient product-line testing using incremental pairwise sampling;towards a software product line of trie-based collections;tool demo: testing configurable systems with FeatureIDE;automated regression testing of BPMN 2.0 processes: a capture and replay framework for continuous delivery;a vision for online verification-validation;and automatic non-functional testing of code generators families.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Temporal NetKAT

引用

acm sigplan NOTICES 2016年第6期51卷 386-401页

作者： Beckett, Ryan Greenberg, Michael Walker, David Princeton Univ Princeton NJ 08544 USA Pomona Coll Claremont CA 91711 USA

Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint-one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet's path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of pathbased correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.

关键词： Software-defined networking Network programming languages Domain-specific languages Kleene algebra with tests NetKAT Temporal logic

来源：评论

学校读者我要写书评

暂无评论

Biomolecular implementation of a Quasi Sliding Mode Feedback Controller based on DNA Strand Displacement Reactions 37

Biomolecular Implementation of a Quasi Sliding Mode Feedback...

引用

37th Annual International conference of the IEEE-Engineering-in-Medicine-and-Biology-Society (EMBC)

作者： Sawlekar, Rucha Montefusco, Francesco Kulkarni, Vishwesh Bates, Declan G. Univ Warwick Ctr Integrat Synthet Biol Coventry CV4 7AL W Midlands England Univ Padua Dept Informat Engn I-35131 Padua Italy

ISBN: (纸本)9781424492701

A fundamental aim of synthetic biology is to achieve the capability to design and implement robust embedded biomolecular feedback control circuits. An approach to realize this objective is to use abstract chemical reaction networks (CRNs) as a programming language for the design of complex circuits and networks. Here, we employ this approach to facilitate the implementation of a class of nonlinear feedback controllers based on sliding mode control theory. We show how a set of two-step irreversible reactions with ultrasensitive response dynamics can provide a biomolecular implementation of a nonlinear quasi sliding mode (QSM) controller. We implement our controller in closed-loop with a prototype of a biological pathway and demonstrate that the nonlinear QSM controller outperforms a traditional linear controller by facilitating faster tracking response dynamics without introducing overshoots in the transient response.

关键词： CRNs Biomolecular implementation Quasi Sliding Mode Feedback Controller based

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：