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

Correspondence Assertions for Process Synchronization in Concurrent Communications

Electronic Notes in Theoretical Computer Science 2004年 97卷 175-195页

作者： Eduardo Bonelli Adriana Compagnoni Elsa Gunter Stevens Institute of Technology and LIFIA Faculty of Informatics University of La Plata La Plata Argentina Stevens Institute of Technology USA New Jersey Institute of Technology USA

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types [Honda, K., V. Vasconcelos and M. Kubo, Language primitives and type discipline for structured communication-based programming, in: Proc. of ESOP'98, LNCS (1998), pp. 122–138]. However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions [Clarke, E. and W. Marrero, Using formal methods for analyzing security, Information Survivability Workshop (1998), Gordon, A. and A. Jeffrey, Typing correspondence assertions for communication protocols, in: seventeenth conference on the mathematical foundations of programming semantics (mfps 2001), number 45 in ENTCS (2001)]. The resulting type discipline augments the types of long term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address the shortcomings present in the pure theory of session types. Keywords: Concurrent programming, pi-calculus, type systems, session types, correspondence assertions.

关键词： Concurrent programming pi-calculus type systems session types correspondence assertions

来源：评论

学校读者我要写书评

暂无评论

Demonstrating lambda calculus reduction

Demonstrating lambda calculus reduction

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Sestoft, Peter Department of Mathematics and Physics Royal Veterinary and Agricultural University Denmark IT University of Copenhagen Denmark

We describe lambda calculus reduction strategies using big-step operational semantics and show how to efficiently trace such reductions. This is used in a web-based lambda calculus reducer, at http://***/~sestoft/lamr... 详细信息

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

A game semantics of idealized CSP

A game semantics of idealized CSP

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Laird, J. COGS University of Sussex Brighton BN1 9QH United Kingdom

A games semantics is described for a typed functional language which includes primitives for parallel composition and for synchronous communication on private channels. The semantics is based on a category obtained by extending "Hyland-Ong games" with a representation of multiple threads of control using "concurrency pointers" which express a new kind of causality relation between moves. The semantics is proved to be fully abstract for "channel-free" types with respect to a may-and-must equivalence for the finitary fragment, and with respect to may-equivalence for the whole language, using factorization results to reduce definability to the sequential case. © 2001 Published by Elsevier Science B.V.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

On extracting static semantics

On extracting static semantics

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Hannan, John Department of Computer Science and Engineering The Pennsylvania State University University Park PA 16802 United States

We examine the problem of automatically extracting a static semantics from a language's semantic definition. Traditional approaches require manual construction of static and dynamic semantics, followed by a proof that the two are consistent. As languages become more complex, the static analyses also become more complex, and consistency proofs have typically been challenging. We need to find techniques for automatically constructing static analyses that are provably correct. © 2001 Published by Elsevier Science B.V.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

Distance and measurement in domain theory

Distance and measurement in domain theory

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Waszkiewicz, Pawel School of Computer Science The University of Birmingham Birmingham United Kingdom

We investigate the notion of distance on domains. In particular, we show that measurement is a fundamental concept underlying partial metrics by proving that a domain in its Scott topology is partially metrizable only if it admits a measurement. Conversely, the natural notion of a distance associated with a measurement not only yields meaningful partial metrics on domains of essential importance in computation, such as IR, Σinfin;and Pω, it also serves as a useful theoretical device by allowing one to establish the existence of partial metrics on arbitrary ω-continuous dcpo's. © 2001 Published by Elsevier Science B.V.

关键词： Computer systems programming

来源：评论

学校读者我要写书评

暂无评论

Pseudo-commutative monads

Pseudo-commutative monads

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Hyland, Martin Power, John Dept of Pure Mathematics and Mathematical Statistics University of Cambridge Wilberforce Road Cambridge United Kingdom Laboratory for the Foundations of Computer Science University of Edinburgh King's Buildings Edinburgh EH9 3JZ United Kingdom

We introduce the notion of pseudo-commutative monad together with that of pseudo-closed 2-category, the leading example being given by the 2-monad on Cat whose 2-category of algebras is the 2-category of small symmetric monoidal categories. We prove that for any pseudo-commutative 2-monad on Cat, its 2-category of algebras is pseudo-closed. We also introduce supplementary definitions and results, and we illustrate this analysis with further examples such as those of small categories with finite products, and examples arising from wiring, interaction, contexts, and the logic of Bunched Implication. © 2001 Published by Elsevier Science B.V.

关键词： Computation theory

来源：评论

学校读者我要写书评

暂无评论

A generalisation of stationary distributions, and probabilistic program Algebra

A generalisation of stationary distributions, and probabilis...

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： McIver, A.K. Department of Computing Macquarie University NSW Australia

We generalise the classical notion of stationary distributions of Markov processes to a model of probabilistic programs which includes demonic nondeterminism. As well as removing some of the conditions normally required for stationarity, our generalisation allows the development of a complete theory linking stationary behaviour to long-term average behaviour - the latter being an important property that lies outside the expressive range of standard logics for probabilistic programs. © 2001 Published by Elsevier Science B.V.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

semantics for algebraic operations

Semantics for algebraic operations

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Plotkin, Gordon Power, John Laboratory for the Foundations of Computer Science University of Edinburgh King's Buildings Edinburgh EH9 3JZ United Kingdom

Given a category C with finite products and a strong monad T on C, we investigate axioms under which an ObC-indexed family of operations of the form αx:(Tx)n &rarr Tx provides a definitive semantics for algebraic operations added to the computational λ-calculus. We recall a definition for which we have elsewhere given adequacy results for both big and small step operational semantics, and we show that it is equivalent to a range of other possible natural definitions of algebraic operation. We outline examples and non-examples and we show that our definition is equivalent to one for call-by-name languages with effects, too. © 2001 Published by Elsevier Science B.V.

关键词： Algebra

来源：评论

学校读者我要写书评

暂无评论

A case study in abstract interpretation based program transformation: Blocking command elimination

A case study in abstract interpretation based program transf...

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Cousot, Patrick Cousot, Radhia Département d'Informatique École Normale Supérieure 45 rue d'Ulm 75230 Paris Cedex 05 France Laboratoire d'Informatique LIX CNRS and École Polytechnique 91128 Palaiseau Cedex France

The design of correct semantics-based program transformations was illustrated using abstract interpretation on blocking code elimination. The general idea to formalize program transformation by abstract interpretation was to define a semantic transformation as an abstraction of the subject program semantics. The correctness of the semantic transformation is proved using an observational abstraction and specify details about the subject and transformed semantics should be abstracted away to considered them as equivalent. It is stated that abstract interpretation can be used to define a semantics-based program transformation framework.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

Regular-language semantics for a call-by-value programming language

Regular-language semantics for a call-by-value programming l...

引用

mfps 2001, seventeenth conference on the mathematical foundations of programming semantics

作者： Ghica, Dan R. Department of Computing and Information Science Queen's University Kingston Ont. K7L 3N6 Canada

We explain how game semantics can be used to reason about term equivalence in a finitary imperative first order language with arrays. For this language, the game-semantic interpretation of types and terms is fully characterized by their sets of complete plays. Because these sets are regular over the alphabet of moves, they are representable by (extended) regular expressions. The formal apparatus of game semantics is greatly simplified but the good theoretical properties of the model are preserved. The principal advantage of this approach is that it is mathematically elementary, while fully formalized. Since language equivalence for regular languages is decidable, this method of proving term equivalence is suitable for automation. © 2001 Published by Elsevier Science B.V.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：