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

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2011年 276卷 191-213页

作者： Jeannin, Jean-Baptiste Cornell Univ Dept Comp Sci Ithaca NY 14853 USA

Capsules are a clean representation of the state of a computation in higher-order programming languages with effects. Their intent is to simplify and replace the notion of closure. They naturally provide support for functional and imperative features, including recursion and mutable bindings, and ensure lexical scoping without the use of closures, heaps, stacks or combinators. We present a comparison of the use of closures and capsules in the semantics of higher-order programming languages with effects. In proving soundness of one to the other, we give a precise account of how capsule environments and closure environments relate to each other.

关键词： Capsule Closure Functional programming Imperative programming State of Computation Higher-Order Functions Mutable Variables Scoping programming language semantics

来源：评论

学校读者我要写书评

暂无评论

A SYNTACTIC THEORY OF MESSAGE PASSING

引用

JOURNAL OF THE ACM 1980年第2期27卷 365-383页

作者： WARD, SA HALSTEAD, RH Laboratory for Computer Science Massachusetts Institute of Technology Cambridge MA Laboratory for Computer Science Massachusetts Institute of Technology Cambridge MA

Recent developments by Hewitt and others have stimulated interest in message-passing constructs as an alternative to the more conventional applicative semantics on which most current languages are based. The present work illuminates the distinction between applicative and message-passing semantics by means of the μ-calculus, a syntactic model of message-passing systems similar in mechanism to the λ-calculus. Algorithms for the translation of expressions from the λ- to the μ-calculus are presented, and differences between the two approaches are ***-passing semantics seem particularly applicable to the study of multiprocessing. The μ-calculus, through the mechanism of conduits, provides a simple model for a limited but interesting class of parallel computations. Multiprocessing capabilities of the μ-calculus are illustrated, and multiple-processor implementations are discussed briefly.

关键词： actor semantics distributed computing lambda calculus message passing programming language semantics

来源：评论

学校读者我要写书评

暂无评论

Data Types as Lattices

引用

SIAM Journal on Computing 1976年第3期5卷 522-587页

作者： Dana Scott

The meaning of many kinds of expressions in programming languages can be taken as elements of certain spaces of “partial” objects. In this report these spaces are modeled in one universal domain PωPω{\bf P} \omega... 详细信息

The meaning of many kinds of expressions in programming languages can be taken as elements of certain spaces of “partial” objects. In this report these spaces are modeled in one universal domain

Pω ${\bf P} \omega$ , the set of all subsets of the integers. This domain renders the connection of this semantic theory with the ordinary theory of number theoretic (especially general recursive) functions clear and straightforward.

关键词： programming language semantics lattice continuous lattice algebraic lattice computability retract combinatory logic lambda calculus recursion theorem enumeration degrees continuous function fixed-point theorem

来源：评论

学校读者我要写书评

暂无评论

Achieving information flow security through monadic control of effects

引用

JOURNAL OF COMPUTER SECURITY 2009年第5期17卷 599-653页

作者： Harrison, William L. Hook, James Univ Missouri Dept Comp Sci Columbia MO 65201 USA Portland State Univ Dept Comp Sci Portland OR 97207 USA

This paper advocates a novel approach to the construction of secure software: controlling information flow and maintaining integrity via monadic encapsulation of effects. This approach is constructive, relying on properties of monads and monad transformers to build, verify, and extend secure software systems. We illustrate this approach by construction of abstract operating systems called separation kernels. Starting from a mathematical model of shared-state concurrency based on monads of resumptions and state, we outline the development by stepwise refinements of separation kernels supporting Unix-like system calls, interdomain communication, and a formally verified security policy (domain separation). Because monads may be easily and safely represented within any pure, higher-order, typed functional language, the resulting system models may be directly realized within a language such as Haskell.

关键词： language-based security monads non-interference programming language semantics information flow security

来源：评论

学校读者我要写书评

暂无评论

GUARDED COMMANDS, NONDETERMINACY AND FORMAL DERIVATION OF PROGRAMS

引用

COMMUNICATIONS OF THE ACM 1975年第8期18卷 453-457页

作者： DIJKSTRA, EW BORROUGHS CORP PLATAAN STR 5NUENEN 4565NETHERLANDS

So-called 'guarded commands' are introduced as a building block for alternative and repetitive constructs that allow nondeterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state. For the formal derivation of programs expressed in terms of these constructs, a calculus will be be shown. [ABSTRACT FROM AUTHOR]

关键词： case-construction correctness proof derivation of programs nondeterminancy program semantics programming language semantics programming languages programming methodology repetition sequencing primitives termination

来源：评论

学校读者我要写书评

暂无评论

INITIAL ALGEBRA semantics AND CONTINUOUS ALGEBRAS

引用

JOURNAL OF THE ACM 1977年第1期24卷 68-95页

作者： GOGUEN, JA THATCHER, JW WAGNER, EG WRIGHT, JB UNIV CALIF LOS ANGELES DEPT COMP SCILOS ANGELESCA 90024 IBM CORP THOMAS J WATSON RES CTRYORKTOWN HTSNY 10598

Many apparently divergent approaches to specifying formal semantics of programming languages are applications of initial algebra semantics. In this paper an overview of initial algebra semantics is provided. The major technical feature is an initial continuous algebra which permits unified algebraic treatment of iterative and recursive semantic features in the same framework as more basic operations.

关键词： algebraic semantics algebras continuous algebras flow diagrams free algebras posets programming language semantics solutions of equations syntax directed translation

来源：评论

学校读者我要写书评

暂无评论

A More Consistent Understanding of Consistency

A More Consistent Understanding of Consistency

引用

Reliable Distributed Systems

作者： Subhajit Sidhanta Ricardo Dias Rodrigo Rodrigues IIT Bhilai India Universidade NOVA de Lisboa Lisbon Portugal INESC-ID/Instituto Superior T??cnico ULisboa

ISBN: (数字)9781728142227

ISBN: (纸本)9781728142234

Recent storage systems trade strong consistency for performance, availability, and scalability. However, this makes it hard to understand the semantics that the storage system provides, and also makes the design and implementation of the storage system itself more error-prone. This paper proposes a comprehensive solution to these problems. In particular, we propose a specification language named ConSpec, which enables the formalization of different consistency semantics that a storage system may provide, using a uniform syntax that is independent of the design and implementation of the target storage system. We use ConSpec to revisit several existing models in light of a common way to define and compare them. Furthermore, we generalize the CAP theorem, whose original formulation only considered linearizability, to precisely define the class of consistency definitions that can and cannot be implemented in a highly-available, partition-tolerant way. Finally, we present the design and implementation of a new consistency checker that takes a trace from a storage system (e.g., the output of a test suite) and validates whether it meets any consistency semantics defined using ConSpec. The evaluation of our consistency checker shows that it is able to verify the correctness of long traces in a reasonable time.

关键词： formal specification formal verification programming language semantics specification languages storage management Cache Memory System specification description language programming language semantics Store management Formal verification consistency Consistency (Measurement) semantics Formal specifications semiotics

来源：评论

学校读者我要写书评

暂无评论

The Fundamentals of Hybrid Systems Modelers

The Fundamentals of Hybrid Systems Modelers

引用

2010 49th IEEE Conference on Decision and Control

作者： Albert Benveniste Benoit Caillaud Marc Pouzet INRIA-Rennes Campus de Beaulieu 35042 Rennes cedex France LIENS Ecole normale superieure 45 rue d'Ulm 75230 Paris Cedex 05 France

ISBN: (纸本)9781424477456

Hybrid systems modelers have become the corner stone of embedded system development, with Simulink a de facto standard and Modelica a new player. Such tools still raise a number of issues that, we believe, require more fundamental understanding. In this paper we propose using non standard analysis as a semantic domain for hybrid systems - non standard analysis is an extension of classical analysis in which infinitesimals (the epsilon and eta in the celebrated generic sentence (arbitrary)(epsilon)(exist)(eta)... in college maths) can be manipulated as first class citizens. This allows us to provide a denotational semantics and a constructive semantics for hybrid systems, thus establishing simulation engines on a firm mathematical basis. In passing, we cleanly separate the job of the numerical analyst (solving differential equations) from that of the computer scientist (generating execution schemes).

关键词： hybrid systems Cornerstones embedded system development non-standard Computer personnel programming language semantics semantics jobs Differential equations

来源：评论

学校读者我要写书评

暂无评论

The formal semantics of the timeER model 06

The formal semantics of the timeER model

引用

Asia-Pacific Conference on Conceptual Modelling

作者： Heidi Gregersen Aarhus School of Business Aarhus V Denmark

ISBN: (纸本)9781920682354

A wide range of database applications manage information that varies over time. Many of the underlying database schemas of these were designed using one of the several versions of the Entity-Relationship (ER) model. In the research community as well as in industry, it is common knowledge that the temporal aspects of the mini-world are pervasive and important, but are also difficult to capture using the ER model. Not surprisingly, several enhancements to the ER model have been proposed in an attempt to more naturally and elegantly support the modeling of temporal aspects of information. Common to most of the existing temporally extended ER models is that the semantics of the models are unclear. This problem is addressed in this paper by developing a formal semantics for the TIMEER model based on denotational semantics.

关键词： temporal semantics entity relationship model Database applications semantics semiotics programming language semantics Aspects(Temporal)

来源：评论

学校读者我要写书评

暂无评论

The derivation of functional equivalents of imperative programs 01

The derivation of functional equivalents of imperative progr...

引用

Australasian Computer Architecture Conference

作者： Graham H. B. Roberts The Flinders University of South Australia

ISBN: (纸本)0769509630

Denotational semantics is presented as a valuable theoretical tool, having many applications including language design, compiler generation and program analysis. In particular, a method is described for deriving a concise and useful functional representation of a program using a denotational definition of the source language's semantics. Our aim is to translate a given program into a compact functional representation to facilitate its evaluation on functional hardware. The λ-expressions are first translated into Turner's combinator code (see [7]). We choose to use a fixed set of combinators as the resulting code is more amenable to analysis and there are many inherent advantages such as lazy evaluation and once only evaluation of reducible sub-expressions. Semantic algebras relating to static semantics and the store algebra are "unfrozen" so they can be partially evaluated. The reduction machine that performs the evaluation includes simplification rules that allows a more compact functional representation (denotation) to be reached. If desired, some or all of the programs arguments can be supplied to produce a new denotation (result) using the same reduction machine.

关键词： derivation FUNCTIONALS original language FUNCTIONAL EQUIVALENT programming language semantics lazy evaluation semantics analysis programme simplification semiotics Algebra TURNER machine language design

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：