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

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

30 篇 会议
18 篇 期刊文献
14 册 图书
2 篇 科技报告

馆藏范围

64 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

40 篇 工学
- 39 篇 计算机科学与技术...
- 19 篇 软件工程
- 2 篇 力学（可授工学、理...
- 1 篇 材料科学与工程（可...
- 1 篇 电气工程
- 1 篇 信息与通信工程
14 篇 理学
- 14 篇 数学
- 2 篇 物理学
3 篇 管理学
- 3 篇 图书情报与档案管...

主题

18 篇 semantics
11 篇 logics and meani...
10 篇 mathematical log...
10 篇 computer program...
8 篇 mathematical log...
7 篇 programming lang...
7 篇 artificial intel...
5 篇 software enginee...
5 篇 software enginee...
4 篇 programming theo...
3 篇 theory of comput...
3 篇 computer program...
3 篇 programming tech...
2 篇 linear logic
2 篇 denotational sem...
2 篇 natural language...
2 篇 computer system ...
2 篇 computation by a...
1 篇 object oriented ...
1 篇 parallelism

机构

2 篇 department of ma...
2 篇 department of co...
2 篇 mathematical sci...
1 篇 department of co...
1 篇 verimag laborato...
1 篇 department of ma...
1 篇 department of ch...
1 篇 philips research...
1 篇 dipartimento di ...
1 篇 computing scienc...
1 篇 department of ma...
1 篇 stevens institut...
1 篇 gec hirst resear...
1 篇 centre for mathe...
1 篇 liens ecole norm...
1 篇 univ penn dept m...
1 篇 colgate universi...
1 篇 computer laborat...
1 篇 department of co...
1 篇 school of comput...

作者

3 篇 mislove michael ...
2 篇 gilmore pc
2 篇 tsiknis gk
1 篇 japaridze giorgi
1 篇 ghelli giorgio
1 篇 zamfir maria
1 篇 dag westerståhl
1 篇 maria garcia de ...
1 篇 bottinger c
1 篇 kent robert e.
1 篇 nielson f
1 篇 mulry ps
1 篇 burn gl
1 篇 de roever w.p.
1 篇 pasztor a
1 篇 axel legay
1 篇 révész györgy e.
1 篇 kung-kiu lau
1 篇 slavnov sergey
1 篇 bainbridge es

语言

64 篇 英文

检索条件"任意字段=Fourth Workshop on Mathematical Foundations of Programming Semantics"

共 64 条记录，以下是41-50 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

Rule-based semantics for an extended lambda-calculus 3rd

Rule-based semantics for an extended lambda-calculus

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Révész, György E. IBM T. J. Watson Research Center Yorktown HeightsNY United States

ISBN: (纸本)9783540190202

Many implementation techniques proposed for functional languages in the literature are based on lambda-calculus and the theory of combinators [5, 12, 14]. The main advantage of functional languages over the more conventional programming languages is their lack of side-effects which makes their semantics much simpler [2]. This paper presents a λ-calculus dialect with list-handling extensions that can be used for defining an operational semantics for functional programs. This semantics is based on a set of elementary α-rules and β-rules which collectively implement the substitution operation without explicitly using it [10]. Two extra reduction rules, called γ-rules, have been added to the system for list manipulations [11]. Combining λ-calculus with list-handling capabilities makes an efficient vectorization of λ-calculus possible. This way we obtain a very elegant treatment of mutual recursion in our system. The reduction rules described in this paper represent, in fact, an operational semantics for our extended λ-notation. An interpreter program for this extended λ-calculus has been developed by a direct implementation of the reduction rules which makes the correctness proof of the interpreter very easy. The notion of controlled reduction is introduced here to guarantee the existence of a normal form for λ-expressions representing recursively defined functions using the Y combinator. © 1988, Springer-Verlag.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

The metric closure powerspace construction 3rd

The metric closure powerspace construction

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Kent, Robert E. Department of Electrical Engineering and Computer Science University of Illinois at Chicago ChicagoIL60680 United States

ISBN: (纸本)9783540190202

In this paper we develop a natural powerobject construction in the context of enriched categories, a context which generalizes the traditional order-theoretic and metric space contexts. This powerobject construction is a subobject transformer involving the dialectical flow of closed subobjects of enriched categories. It is defined via factorization of a comprehension schema over metrical predicates, followed by the fibrational inverse image of metrical predicates along character, the left adjoint in the comprehension schema. A fundamental continuity property of this metrical powerobject construction vis-a-vis greatest fixpoints is established by showing that it preserves the limit of any Cauchy ωop-diagram. Using this powerobject construction we unify two well-known fixpoint semantics for concurrent interacting processes. © 1988, Springer-Verlag.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

On the Smyth power domain 3rd

On the Smyth power domain

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Mislove, Michael Department of Mathematics Tulane University New OrleansLA70118 United States

ISBN: (纸本)9783540190202

This paper explores the connection between the Smyth power domain PS(D) of a domain D and the domain D itself. The Smyth power domain is the most prevalent of the three power domain constructions commonly used to model nondeterminism in the denotational semantics of high-level programming languages. One definition of the Smyth power domain PS(D) is as the set of all Lawson-closed upper sets X from the domain D, so there is the natural inclusion x ↦↑x: D → PS(D). On the other hand, the inf map X ↦ ∧ X: PS(D) → D is an upper adjoint to this inclusion, and we use this adjunction to obtain information about PS(D) from the domain D. If D is distributive, spectral theory implies that each element X of PS(D) satisfies ∧ X is the infimum of a unique set of primes minimal with respect to being contained in X. Results which characterize when a domain D does not contain a copy of 2N are invoked to show that the set of such primes is finite in certain cases. We indicate how these results can be generalized to the case that D is locally distributive or semiprime. Our results are motivated by an interest in understanding the Smyth power domain PS(D) in terms of the domain D, and we feel they should have application to the semantics of high-level programming languages. An indication of some possible applications of these results is given at the end of the paper. © 1988, Springer-Verlag.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

Assertional categories 3rd

Assertional categories

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Manes, Ernie Department of Mathematics and Statistics Lederle Research Center Tower University of Massachusetts AmherstMA01003 United States

ISBN: (纸本)9783540190202

Assertional categories provide a general algebraic framework for the denotation of programs. While the axioms deal exclusively with the abstract structure of coproducts, it is possible to express Boolean structure, loop-free constructs and predicate transformers and to deduce basic properties associated with propositional dynamic logic. At the foundational level, new "quarks" to build the atomic constructions of programs are espoused, leading to a new categorical duality principle for predicate transformers (based on a semilattice completion by ideals) and to the "grand unification principle" that "composition determines semantics". The first-order theory of assertional categories is more general than dynamic logic in that nondeterminism may include repetition count, that is, f + f need not be f. On the other hand, an adaptation of a theorem of Kozen shows that, at least for iteration-free sentences about predicate transformers, semantics is standard. Several algebraic characterizations of Dijkstra's definition of determinism are offered and one leads to a technique to reduce loop-free expressions to guarded commands. Axioms for iteration include a "uniformity principle" that "related programs have related iterates" and the Segerburg induction axiom follows. © 1988, Springer-Verlag.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

dI-domains as a model of polymorphism 3rd

dI-domains as a model of polymorphism

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Coquand, Thierry Gunter, Carl Winskel, Glynn Computer Laboratory University of Cambridge CambridgeCB2 3QG United Kingdom

ISBN: (纸本)9783540190202

In this paper we investigate a model construction recently described by Jean Yves Girard. This model differs from the models of McCracken, Scott, etc. in that the types are interpreted (quite pleasingly) as domains rather than closures or finitary projections on a universal domain. Our objective in this paper is two-fold. First, we would like to generalize Girard's construction to a larger category called dI-domains which was introduced by Berry [2]. The dI-domains possess many of the virtues of the domains used by Girard. Moreover, the dI-domains are closed under the separated sum and lifting operators from denotational semantics and this is not true of the domains of Girard. We intend to demonstrate that our generalized construction can be used to do denotational semantics in the ordinary way, but with the added feature of type polymorphism with a "types as domains" interpretation. Our second objective is to show how Girard's construction (and our generalization) can be done abstractly. We also give a representational description of our own construction using the notion of a prime event structure. © 1988, Springer-Verlag.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

Initial algebra semantics and concurrency 3rd

Initial algebra semantics and concurrency

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Zamfir, Maria Computer Science Department KSU ManhattanKS66506 United States

ISBN: (纸本)9783540190202

The purpose of this paper is to show that initial algebra semantics has an immediate and useful application in the area of communicating computing systems. The major technical feature is a category of continuous many-sorted algebras ca led parallel-nondeterministic algebras. In this setting parallel and nondeterministic behaviors of communicating computing systems can be rigorously formulated as sequences of rewritings on abstract objects called parallel-nondeterministic terms or diamonds. It is shown that diamonds are free in the category of continuous parallel-nondeterministic algebras. (To demonstrate this fact, some results concerning categories of continuous algebras, which can be found in the work of the ADJ group, are presented in a self-contained form.) Nondeterminism and parallelism are modeled explicitly by introducing a choice operator and a parallel operator, respectively. In a companion paper [10] flow nets are introduced to describe parallel and nondeterministic behaviors of computing systems that communicate with each other, just as conventional flowcharts are used to describe sequential computations. In a continuous parallel-nondeterministic algebra a flow net is represented by its unfoldment — the solution of a finite system of recursive equations. © 1988, Springer-Verlag.

关键词： Algebra

来源：评论

学校读者我要写书评

暂无评论

Path semantics 3rd

Path semantics

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Bloss, Adrienne Hudak, Paul Yale University New HavenCT06520 United States

ISBN: (纸本)9783540190202

Knowledge of order of evaluation of expressions is useful for compile-time optimizations for lazy sequential functional programs. We present path semantics, a non-standard semantics that describes order of evaluation for a first-order functional language with lazy evaluation. We also provide an effective abstraction of path semantics that provides compile-time information. We show how path semantics may be used in strictness analysis, process scheduling in parallel systems, and optimized self-modifying thunks. © 1988, Springer-Verlag.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

The semantics of Miranda's algebraic types 3rd

The semantics of Miranda's algebraic types

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Bruce, Kim B. Riecke, Jon G. Department of Computer Science Williams College WilliamstownMA01267 United States MIT Laboratory for Computer Science 545 Technology Square CambridgeMA02139 United States

ISBN: (纸本)9783540190202

Miranda has two interesting features in its typing system: implicit polymorphism (also known as ML-style polymorphism) and algebraic types. Algebraic types create new types from old and can operate on arbitrary types. This paper argues that functions on types, or type constructors, best represent the meaning of algebraic types. Building upon this idea, we develop a denotational semantics for algebraic types. We first define a typed lambda calculus that specifies type constructors. A semantic model of type constructors is then built, using the ideal model as a basis. (The ideal model gives the most natural semantics for Miranda's implicit polymorphism.) The model is shown to be sound with respect to this lambda calculus. Finally, we demonstrate how to use the model to interpret algebraic types, and prove that the translation produces elements in the model. © 1988, Springer-Verlag.

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

Semantically based axiomatics 3rd

Semantically based axiomatics

引用

3rd workshop on the mathematical foundations of programming Language semantics, 1987

作者： Brookes, Stephen D. Department of Computer Science Carnegie-Mellon University PittsburghPA15213 United States

ISBN: (纸本)9783540190202

This paper discusses some fundamental issues related to the construction of semantically based axiomatic proof systems for reasoning about program behavior. We survey foundational work in this area, especially early work of Hoare and Cook on while-programs, and we try to pinpoint the principal ideas contained in this work and to suggest criteria for an appropriate generalization (faithful to these ideas) to a wider variety of programming languages. We argue that the adoption of a mathematically clean semantic model should lead to a natural choice of assertion language(s) for expressing properties of program terms, and to syntax-directed proof systems with clear and simple rules for program constructs. Hoare's ideas suggest that in principle syntax-directed reasoning is possible for all syntactic categories (declarations, commands, even expressions) and all semantic attributes (partial correctness of commands, aliasing properties of declarations, L- or R-values of expressions, proper use of variables, and so on). Semantic insights may also influence assertion language design by suggesting the need for certain logical connectives at the assertion level. This point is obscured by the fact that Hoare's logic for while-programs needed no assertion connectives (although of course the usual logical connectives are permitted inside pre- and post-conditions), but an application of our method to a class of parallel programming languages brings out the idea well: semantic analysis suggests the use of conjunctions at the assertion level. We argue that this method can lead to proof systems which avoid certain inelegant features of some earlier systems: specifically, we avoid the need for "extralogical" and "non-compositional" notions such as interference checks and auxiliary variables. We also discuss the author's applications of these techniques to other programming languages, and point to some future research directions continuing this work. Although we do not have a completel

关键词： semantics

来源：评论

学校读者我要写书评

暂无评论

The theory of strictness analysis for higher order functions

The theory of strictness analysis for higher order functions

引用

workshop on Programs as Data Objects, 1985

作者： Burn, Gl Hankin, Cl Abramsky, S. GEC Hirst Research Centre East Lane WembleyMiddxHA9 7PP United Kingdom Department of Computing Imperial College of Science and Technology 180 Queen's Gate LondonSW7 2BZ United Kingdom

ISBN: (纸本)9783540164463

Abstract interpretation is a compile-time technique which is used to gain information about a program that may then be used to optimise the execution of the program. A particular use of abstract interpretation is in strictness analysis of functional programs. This provides the key to the exploitation of parallelism in the evaluation of programs written in functional languages. In a language that has lazy semantics, the main potential for parallelism arises in the evaluation of operands of strict operators. A function is strict in an argument if its value is undefined whenever the argument is undefined. If we can use strictness analysis to detect which arguments a function is strict in, we then know that these arguments can be safely evaluated in parallel because this will not affect the lazy semantics. Experimental results suggest that this leads to significant speed-ups. Mycroft was the first person to apply abstract interpretation to the strictness analysis of functional programs. His framework only applies to first-order functions on flat domains. Several workers have proposed practical approaches to strictness analysis of higher-order functions over flat base domains but their work has not been accompanied by extensions to Mycroft's theoretical framework. In this paper we give sound mathematical foundations for this work and discuss some of the practical issues involved. The practical approach is proved correct in relation to the theoretical framework. © 1986, Springer-Verlag.

关键词： Functional programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共7页 << < 1 2 3 4 5 6 7 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：