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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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

分类表

所选分类

>> <<

限定检索结果

文献类型

646 篇 会议
75 篇 期刊文献
1 册 图书

馆藏范围

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

日期分布

学科分类号

598 篇 工学
- 463 篇 软件工程
- 447 篇 计算机科学与技术...
- 44 篇 控制科学与工程
- 36 篇 电气工程
- 18 篇 信息与通信工程
- 8 篇 建筑学
- 6 篇 电子科学与技术（可...
- 4 篇 材料科学与工程（可...
- 4 篇 动力工程及工程热...
- 4 篇 土木工程
- 4 篇 生物工程
- 3 篇 化学工程与技术
- 3 篇 农业工程
- 2 篇 力学（可授工学、理...
- 2 篇 石油与天然气工程
- 2 篇 生物医学工程（可授...
94 篇 理学
- 47 篇 数学
- 36 篇 生物学
- 5 篇 系统科学
- 4 篇 物理学
- 3 篇 化学
- 2 篇 统计学（可授理学、...
29 篇 教育学
- 29 篇 教育学
- 14 篇 心理学(可授教育学...
22 篇 管理学
- 16 篇 图书情报与档案管...
- 8 篇 管理科学与工程(可...
- 7 篇 工商管理
19 篇 法学
- 19 篇 社会学
3 篇 经济学
- 3 篇 应用经济学
3 篇 农学
- 3 篇 作物学
1 篇 医学
1 篇 军事学
1 篇 艺术学

主题

96 篇 functional progr...
74 篇 languages
50 篇 genetic programm...
46 篇 design
45 篇 computer program...
30 篇 haskell
27 篇 computer program...
25 篇 programming
21 篇 theory
20 篇 dependent types
19 篇 performance
16 篇 algorithms
15 篇 parallel program...
15 篇 programming lang...
14 篇 logic programmin...
14 篇 functional react...
13 篇 verification
12 篇 object oriented ...
12 篇 domain-specific ...
11 篇 education

机构

8 篇 northeastern uni...
7 篇 portland state u...
6 篇 carnegie mellon ...
6 篇 microsoft res ca...
5 篇 chalmers univ te...
4 篇 inria
4 篇 univ penn philad...
3 篇 indiana univ blo...
3 篇 delft univ techn...
3 篇 univ edinburgh e...
3 篇 open university ...
3 篇 microsoft res re...
3 篇 univ strathclyde...
3 篇 univ new s wales...
3 篇 carnegie mellon ...
3 篇 univ cambridge c...
3 篇 technion-israel ...
3 篇 univ utah salt l...
3 篇 univ chicago il ...
3 篇 yale univ dept c...

作者

6 篇 findler robert b...
5 篇 flatt matthew
5 篇 jones mark p.
5 篇 krishnaswami nee...
4 篇 o'reilly una-may
4 篇 xi hw
4 篇 mcbride conor
4 篇 devriese dominiq...
4 篇 vafeiadis viktor
4 篇 weirich stephani...
4 篇 spector lee
4 篇 claessen koen
4 篇 jeuring johan
4 篇 wu nicolas
4 篇 chlipala adam
4 篇 dreyer derek
4 篇 keller gabriele
4 篇 walker david
3 篇 dolstra eelco
3 篇 loh andres

语言

653 篇 英文
65 篇 其他
2 篇 葡萄牙文
2 篇 中文

检索条件"任意字段=14th ACM SIGPLAN International Conference on Functional Programming"

共 722 条记录，以下是71-80 订阅

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

详细简洁

排序：

Mtac: A Monad for Typed Tactic programming in Coq 13

Mtac: A Monad for Typed Tactic Programming in Coq

引用

18th acm sigplan international conference on functional programming

作者： Ziliani, Beta Dreyer, Derek Krishnaswami, Neelakantan R. Nanevski, Aleksandar Vafeiadis, Viktor MPI-SWS Saarbruecken Germany IMDEA Software Institute Madrid Spain MPI-SWS Kaiserslautern Germany

ISBN: (纸本)9781450323260

Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers. We present Mtac, a lightweight but powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.

关键词： Interactive theorem proving custom proof automation Coq monads typed meta-programming tactics

来源：评论

学校读者我要写书评

暂无评论

A Fresh Look at programming with Names and Binders 10

A Fresh Look at Programming with Names and Binders

引用

15th acm sigplan international conference on functional programming

作者： Pouillard, Nicolas Pottier, Francois INRIA Paris France

ISBN: (纸本)9781605587943

A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms which allow performing these manipulations in a safe and natural style has, to a large extent, remained elusive. In this paper, we present a novel approach to the problem. Our proposal can be viewed either as a programming language design or as a library: in fact, it is currently implemented within Agda. It provides a safe and expressive means of programming with names and binders. It is abstract enough to support multiple concrete implementations: we present one in nominal style and one in de Bruijn style. We use logical relations to prove that "well-typed programs do not mix names with different scope". We exhibit an adequate encoding of Pitts-style nominal terms into our system.

关键词： names binders meta-programming name abstraction higher-order abstract syntax

来源：评论

学校读者我要写书评

暂无评论

COP 2022 - Proceedings of the 14th international Workshop on Context-Oriented programming and Advanced Modularity, Co-located with ECOOP 2022

COP 2022 - Proceedings of the 14th International Workshop on...

引用

14th international Workshop on Context-Oriented programming and Advanced Modularity, COP 2022 - Co-located with ECOOP 2022

ISBN: (纸本)9781450399869

the proceedings contain 6 papers. the topics discussed include: layer activation mechanism for asynchronous executions in JavaScript;explicit tool support for implicit layer activation;modeling flexible monitoring systems with a role-based control loop;guard the cache: dispatch optimization in a contextual role-oriented language;generating virtual scenarios for cyber ranges from feature-based context-oriented models: a case study;and a step toward programming with versions in real-world functional languages.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Tangible functional programming

Tangible functional programming

引用

12th acm sigplan international conference on functional programming

作者： Elliott, Conal M. LambdaPix

ISBN: (纸本)9781595938152

We present a user-friendly approach to unifying program creation and execution, based on a notion of "tangible values" (TVs), which are visual and interactive manifestations of pure values, including functions. programming happens by gestural composition of TVs. Our goal is to give end-users the ability to create parameterized, composable content without imposing the usual abstract and linguistic working style of programmers. We hope that such a system will put the essence of programming into the hands of many more people, and in particular people with artistic/visual creative style. In realizing this vision, we develop algebras for visual presentation and for "deep" function application, where function and argument may both be nested within a structure of tuples, functions, etc. Composition gestures are translated into chains of combinators that act simultaneously on statically typed values and their visualizations.

关键词： human factors languages theory interactive programming end-user programming gestural composition combinator libraries arrows interactive visualization

来源：评论

学校读者我要写书评

暂无评论

Multi-polymorphic programming in bondi

Multi-polymorphic programming in bondi

引用

2013 9th acm sigplan Workshop on Generic programming, WGP 2013 - Co-located with the 18th acm sigplan international conference on functional programming, ICFP 2013

作者： Given-Wilson, thomas Huang, Freeman Jay, Barry NICTA Australia University of Technology Sydney Australia

ISBN: (纸本)9781450323895

the bondi programming language is multi-polymorphic, in that it supports four polymorphic programming styles within a small core of computation, namely a typed pattern calculus. bondi's expressive power is illustrated by considering the problem of assigning reviewers to a paper. As the context generalises from a committee to a committee with additional reviewers, to a conference, to a federation or confederation, the solution incorporates polymorphism familiar from the functional, generic functional, relational, path-based, and object-oriented programming styles, respectively. these experiments show that multi-polymorphic programming is both practical and desirable. Copyright © 2013 acm.

关键词： Pattern matching

来源：评论

学校读者我要写书评

暂无评论

Productive Coprogramming with Guarded Recursion 13

Productive Coprogramming with Guarded Recursion

引用

18th acm sigplan international conference on functional programming

作者： Atkey, Robert McBride, Conor Univ Strathclyde Glasgow G1 1XQ Lanark Scotland

ISBN: (纸本)9781450323260

Total functional programming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to terminate, e. g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a program generates an infinite amount of data, each piece will be generated in finite time. the theoretical underpinning for productive programming with infinite output is provided by the category theoretic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well-founded data like finite lists and trees. Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compositional, and severely complicate coprogramming. Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to coprogramming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano's guarded recursion. Clock variables allow us to "close over" the generation of infinite codata, and to make finite observations, something that is not possible with guarded recursion alone.

关键词： Languages theory Types Recursion coalgebras corecursion guarded recursion total functional programming

来源：评论

学校读者我要写书评

暂无评论

Partial Memoization of Concurrency and Communication

Partial Memoization of Concurrency and Communication

引用

14th acm sigplan international conference on functional programming

作者： Ziarek, Lukasz Sivararnakrishnan, K. C. Jagannathan, Suresh Purdue Univ Dept Comp Sci W Lafayette IN 47907 USA

ISBN: (纸本)9781605583327

Memoization is a well-known optimization technique used to eliminate redundant calls for pure functions. If a call to a function f with argument 1, yields result r, a subsequent call to f with v can be immediately reduced to r without the need to re-evaluate f's body. Understanding memoization in the presence of concurrency and communication is significantly more challenging. For example, if f communicates with other threads, it is not sufficient to simply record its input/output behavior;we must also track inter-thread dependencies induced by these communication actions. Subsequent calls to f can be elided only if we can identify an interleaving of actions from these call-sites that lead to states in which these dependencies are satisfied. Similar issues arise if f spawns additional threads. In this paper, we consider the memoization problem for a higher-order concurrent language whose threads may communicate through synchronous message-based communication. To avoid the need to perform unbounded state space search that may be necessary to determine if all communication dependencies manifest in an earlier call can be satisfied in a later one, we introduce a weaker notion of memoization called partial memoization that gives implementations the freedom to avoid performing some part, if not all, of a previously memoized call. To validate the effectiveness of our ideas, we consider the benefits of memoization for reducing the overhead of recomputation for streaming, server-based, and transactional applications executed on a multi-core machine. We show that on a variety of workloads, memoization can lead to substantial performance improvements without incurring high memory costs.

关键词： Concurrent programming Partial Memoization Software Transactions Concurrent ML Multicore Systems

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

the Role of C in the Dark Ages of Multi-core

The Role of C in the Dark Ages of Multi-core

引用

14th acm sigplan/SIGBED conference on Languages, Compilers and Tools for Embedded Systems

作者： Beemster, Marcel ACE Associated Compiler Experts bv Netherlands

ISBN: (纸本)9781450320856

Contrary to predictions of its demise, C remains a dominant programming language, especially in embedded systems. Speed and transparency dictate that it will be so for the next decade, despite its supposed unsuitability for programming parallel architectures. A flexible compiler development system is a unique vehicle to bend the C language and its implementation to the developers' will. Using hard-won experience in applying extended versions of C to diverse parallel architectures, C's potential in the dark ages of multi-core programming is examined.

关键词： Languages Performance C programming language multi-core mapping implementation efficiency

来源：评论

学校读者我要写书评

暂无评论

Experience Report: Growing programming Languages for Beginning Students 10

Experience Report: Growing Programming Languages for Beginni...

引用

15th acm sigplan international conference on functional programming

作者： Crestani, Marcus Sperber, Michael Univ Tubingen D-72074 Tubingen Germany

ISBN: (纸本)9781605587943

A student learning how to program learns best when the programming language and programming environment cater to her specific needs. these needs are different from the requirements of a professional programmer. Consequently, the design of teaching languages poses challenges different from the design of "professional" languages. Using a functional language by itself gives advantages over more popular, professional languages, but fully exploiting these advantages requires careful adaptation to the needs of the students-as-is, these languages do not support the students nearly as well as they could. this paper describes our experience adopting the didactic approach of How to Design Programs, focussing on the design process for our own set of teaching languages. We have observed students as they try to program as part of our introductory course, and used these observations to significantly improve the design of these languages. this paper describes the changes we have made, and the journey we took to get there.

关键词： Introductory programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共73页 << < 4 5 6 7 8 9 10 11 12 13 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：