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

LFM 2002 International Workshop on Logical Frameworks and Meta-Languages (FLoC Satellite Event)

作者： Delahaye, David Programming Logic Group Department of Computing Science Chalmers University of Technology S-412 96 Gothenburg Sweden

We describe a proof dedicated meta-language, called Ltac, in the context of the Coq proof assistant. This new layer of meta-language is quite appropriate to write small and local automations. Ltac, is essentially a small functional core with recursors and powerful pattern-matching operators for Coq terms but also for proof contexts. As Ltac, is not complete, we describe an interface between Ltac, and the full programmable meta-language of the system (Objective CAML), which is also the implementation language. This interface is based on a quotation system where we can use Ltac,'s syntax in ML files, and where it is possible to insert ML code in Ltac, scripts by means of antiquotations. In that way, the two meta-languages are not opposed and we give an example where they fairly cooperate. Thus, this shows that a LCF-like system with a two-level meta-language is completely realistic. © 2002 Published by Elsevier Science B. V.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Selector table indexing & sparse arrays 8

Selector table indexing & sparse arrays

引用

8th Annual Conference on Object-Oriented programming Systems, Languages, and Applications, OOPSLA 1993

作者： Driesen, Karel Programming Technology Lab Faculty of Sciences Vrije Universiteit Brussel Pleinlaan 2 BrusselsB-1050 Belgium

ISBN: (纸本)0897915879

Selector table indexing is a simple technique for method lookup in object-oriented languages, which yields good performance, is well suited to multiple inheritance and dynamic typing, but is generally disregarded for its prohibitive memory consumption. The large memory footprint is caused by keeping a table of methods, indexed by a selectorcode, for each class in the system. These tables are sparsely filled. A sparse array implementation is presented, which reduces the memory consumption by an order of magnitude, while performing retrieval in constant time. This implementation is discussed in the context of a real programming environment, and compared to selector coloring, a different memory-optimizing technique. The method is shown to be complementary to dynamic caching techniques such as inline caching. © 1993 ACM.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Lambda lifting: Transforming programs to recursive equations 2nd

引用

2nd International Conference on Functional programming Languages and Computer Architecture, 1985

作者： Johnsson, Thomas Programming Methodology Group Department of Computer Science Chalmers University of Technology GöteborgS-412 96 Sweden

ISBN: (纸本)9783540159759

Lambda lifting is a technique for transforming a functional program with local function definitions, possibly with free variables in the function definitions, into a program consisting only of global function (combinator) definitions which will be used as rewrite rules. Different ways of doing lambda lifting are presented, as well as reasons for rejecting or selecting the method used in our Lazy ML compiler. A functional program implementing the chosen algorithm is given. © 1985, Springer-Verlag.

关键词： Computers

来源：评论

学校读者我要写书评

暂无评论

A technical overview of the information resource dictionary system

引用

Computers and Standards 1985年第3期4卷 153-208页

作者： Goldfine, Alan Konig, Patricia U.S. Department of Commerce National Bureau of Standards Center for Programming Science and Technology Gaithersburg MD 20899 United States

This publication provides a technical overview of the computer software specifications for an Information Resource Dictionary System (IRDS). It summarizes the data architecture and the software functions and processes of the IRDS. The IRDS Specifications are a draft proposed American National Standard, a draft proposed U.S. Federal Information Processing Standard, and a Working Document of the International Organization for Standardization (ISO), Subcommittee 21, Working Group 3. The Overview also provides background information on the development of the draft proposed U.S. standards. © 1985.

关键词： American National Standard Computer software Data dictionary Data dictionary system Data management Federal Information Processing Standard Information Resource Dictionary System Information resource management International Standard IRDS IRM

来源：评论

学校读者我要写书评

暂无评论

Development environment for layout design of e-commerce applications using block-based approach

Development environment for layout design of e-commerce appl...

引用

2011 International Conference on Electrical Engineering and Informatics, ICEEI 2011

作者： Rawi, Nor Haimimy Marini, Abu Bakar Bahari, Rokiah Zin, Abdullah Mohd Programming and Software Technology Research Group Fakulti Teknologi Dan Sains Maklumat Universiti Kebangsaan Malaysia Malaysia

ISBN: (纸本)9781457707520

E-commerce is a process of buying, selling, transferring or exchanging products or services via the Internet. It is expected that in the future, more and more business transactions will be carried out through e-commerce. The design of an e-commerce website plays a significant role in attracting potential customers to visit the site. It can also influence customer's decision to make purchase and to return to the site. Good e-commerce applications need to be developed by professional programmers and the cost is substantially high. With the advent of Web 2.0 technology, end-users are now able to create their own web content and applications such as blog, facebook and friendster. Some providers such as Google provide a mechanism for end-users to create web sites and host e-commerce applications. However, using these technologies, users can only select and customize the application according to provide templates. One of the main problems with this approach is that they do not support a flexible layout design. This implies that an end-user cannot change the layout of a selected template. This paper presents a flexible and easy to use block-based development environment for creating customized e-commerce applications. A block is a single layer software component that performs a single function. Concurrent project has developed blocks for e-commerce application. The proposed development environment is intended for non-programmer end-users to design and develop their own e-Commerce applications by selecting and positioning blocks on a page. © 2011 IEEE.

关键词： Electronic commerce

来源：评论

学校读者我要写书评

暂无评论

Using types as search keys in function libraries

引用

Journal of Functional programming 1991年第1期1卷 71-89页

作者： Rittri, Mikael Programming Methodology Group Department of Computer Sciences Chalmers University of Technology and University of Goteborg S-412 96 Göteborg Sweden

A method is proposed to search for an identifier in a functional program library by using its Hindley-Milner type as a key. This can be seen as an approximation of using the specification as a key. Functions that only differ in their argument order or currying are essentially the same, which is expressed by a congruence relation on types. During a library search, congruent types are identified. If a programmer is not satisfied with the type of a found value, he can use a conversion function (like curry), which must exist between congruent types, to convert the value into the type of his choice. Types are congruent if they are isomorphic in all cartesian closed categories. To put it more simply, types are congruent if they are equal under an arithmetical interpretation, with cartesian product as multiplication and function space as exponentiation. This congruence relation is characterized by seven equational axioms. There is a simple term-rewriting algorithm to decide congruence, using which a search system has been implemented for the functional language Lazy ML, with good performance. The congruence relation can also be used as a basis for other search strategies, e.g. searching for identifiers of a more general type, modulo congruence or allowing free type variables in queries. © 1991, Cambridge University Press. All rights reserved.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Security goals assurance based on software active monitoring

Security goals assurance based on software active monitoring

引用

International Conference on Secure Software Integration and Reliability Improvement

作者： Zhao, Changzhi Dong, Wei Leucker, Martin Qi, Zhichang Department of Computer Science National University of Defense Technology Changsha 410073 China Institute of Software Technology and Programming Languages University of Lubeck Germany

ISBN: (纸本)9780769544533

Access control is a vital security mechanism in today's operating systems and the security policies dictating the security relevant behaviors is lengthy and complex for example in Security-Enhanced Linux (SELinux). It is extremely difficult to verify the consistency between the security policies and the security goals desired by applications. In this paper we present how to predict whether the information flow security goal is violated or not during runtime how to generate the corresponding control actions on-line when divergence is detected and how to apply these actions in time based on software active monitoring technique. The symbolic security information flow model of SElinux is generated from a formalization of the access control mechanism which can be used to generate the N-step ahead projection of the future behavior. Information flow security goals are expressed in linear temporal logic (LTL) which provides clear description of the objectives desired by applications. Anticipatory monitor is generated from LTL formula automatically. We consider an on-line scheme where after the occurrence of an event, the next control action is determined on the basis of the N-step ahead projection of the future behavior. This procedure is repeated after the occurrence of next security relevant event. Thus a closed-loop system is generated that all behavior sequences will satisfy the security goals. © 2011 IEEE.

关键词： Access control

来源：评论

学校读者我要写书评

暂无评论

A succinct canonical register automaton model for data domains with binary relations

A succinct canonical register automaton model for data domai...

引用

10th International Symposium on Automated technology for Verification and Analysis, ATVA 2012

作者： Cassel, Sofia Jonsson, Bengt Howar, Falk Steffen, Bernhard Dept. of Information Technology Uppsala University Sweden Department of Programming Systems Technical University Dortmund Germany

ISBN: (纸本)9783642333859

We present a novel canonical automaton model for languages over infinite data domains, that is suitable for specifying the behavior of services, protocol components, interfaces, etc. The model is based on register automata. A major contribution is a construction of succinct canonical register automata, which is parameterized on the set of relations by which elements in the data domain can be compared. We also present a Myhill Nerode-like theorem, from which minimal canonical automata can be constructed. This canonical form is as expressive as general deterministic register automata, but much better suited for modeling in practice since we lift many of the restrictions on the way variables can be accesed and stored: this allows our automata to be significantly more succinct than previously proposed canonical forms. Key to the canonical form is a symbolic treatment of data languages, which allows us to construct minimal representations whenever the set of relations can be equipped with a so-called branching framework. © 2012 Springer-Verlag.

关键词： Automata theory

来源：评论

学校读者我要写书评

暂无评论

Automated Refactoring to Reactive programming

Automated Refactoring to Reactive Programming

引用

IEEE International Conference on Automated Software Engineering (ASE)

作者： Mirko Köhler Guido Salvaneschi Technische Universitat Darmstadt Darmstadt Germany Reactive Programming Technology Technische Universität Darmstadt Darmstadt Germany

Reactive programming languages and libraries, such as ReactiveX, have been shown to significantly improve software design and have seen important industrial adoption over the last years. Asynchronous applications - which are notoriously error-prone to implement and to maintain - greatly benefit from reactive programming because they can be defined in a declarative style, which improves code clarity and extensibility. In this paper, we tackle the problem of refactoring existing software that has been designed with traditional abstractions for asynchronous programming. We propose 2Rx, a refactoring approach to automatically convert asynchronous code to reactive programming. Our evaluation on top-starred GitHub projects shows that 2Rx is effective with the most common asynchronous constructs, covering 12.7% of projects with asynchronous computations, and it can provide a refactoring for 91.7% of their occurrences.

关键词： programming Java Observers Libraries Instruction sets Loading

来源：评论

学校读者我要写书评

暂无评论

Implementing readers/writers problem using aspect-oriented framework

Implementing readers/writers problem using aspect-oriented f...

引用

2008 International Conference on Software Engineering Research and Practice, SERP 2008

作者： Netinant Computer Science Department, P. Bangkok University Bangkok Thailand Concurrent Programming Research Group Illinois Institute of Technology Chicago IL United States

ISBN: (纸本)1601320884

programming in a distributed environment is a complex activity. Programmers need to be aware of issues unrelated to their domain of problem, and are often unprepared for the challenges the concurrent programming brings. The interaction of their components becomes more complex, and makes it difficult to validate the design and correctness of the system. Supporting separation of concerns in the design and implementation of operating systems can provide a number of benefits such as comprehension, reusability, extensibility and adaptability in both design and implementation. We have tackled this problem by adopting the technique of separation of concerns in concurrent programming. In this paper we demonstrate an Aspect- Oriented Framework (ACL) that can be used for system software such as operating systems. We also show how the separation of system aspectual properties from components. Readers/Writers problem is demonstrated using our framework. Our framework, which is based on aspect- oriented technology as well as language and architecture independence, is a component based model.

关键词： Reusability

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：