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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

445 篇 会议
42 篇 期刊文献
2 册 图书

馆藏范围

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

日期分布

学科分类号

381 篇 工学
- 370 篇 软件工程
- 244 篇 计算机科学与技术...
- 19 篇 控制科学与工程
- 14 篇 电气工程
- 8 篇 信息与通信工程
- 4 篇 建筑学
- 3 篇 电子科学与技术（可...
- 3 篇 农业工程
- 2 篇 力学（可授工学、理...
- 2 篇 材料科学与工程（可...
- 2 篇 动力工程及工程热...
- 2 篇 土木工程
- 1 篇 光学工程
- 1 篇 化学工程与技术
- 1 篇 石油与天然气工程
- 1 篇 生物医学工程（可授...
- 1 篇 生物工程
68 篇 理学
- 64 篇 数学
- 2 篇 物理学
- 2 篇 化学
- 2 篇 生物学
- 2 篇 统计学（可授理学、...
- 1 篇 系统科学
30 篇 管理学
- 27 篇 图书情报与档案管...
- 7 篇 管理科学与工程(可...
- 5 篇 工商管理
3 篇 法学
- 3 篇 社会学
3 篇 农学
- 3 篇 作物学
1 篇 经济学
- 1 篇 应用经济学

主题

81 篇 functional progr...
54 篇 computer program...
39 篇 languages
33 篇 computer program...
24 篇 design
22 篇 haskell
17 篇 object oriented ...
17 篇 logic programmin...
16 篇 dependent types
15 篇 computer systems...
13 篇 programming theo...
13 篇 functional react...
12 篇 generic programm...
12 篇 theory
11 篇 performance
10 篇 domain-specific ...
10 篇 programming lang...
7 篇 ml
7 篇 type theory
7 篇 algorithms

机构

4 篇 northeastern uni...
4 篇 chalmers univ of...
4 篇 portland state u...
4 篇 chalmers univ te...
4 篇 microsoft res ca...
3 篇 inria
3 篇 univ edinburgh e...
3 篇 carnegie mellon ...
3 篇 inria rocquencou...
3 篇 carnegie mellon ...
3 篇 univ cambridge c...
3 篇 microsoft resear...
3 篇 univ penn philad...
3 篇 univ of pennsylv...
3 篇 yale univ dept c...
2 篇 microsoft resear...
2 篇 univ of amsterda...
2 篇 ecole polytech f...
2 篇 tohoku univ send...
2 篇 indiana univ blo...

作者

6 篇 weirich stephani...
5 篇 danvy olivier
5 篇 hanus michael
4 篇 kiselyov oleg
4 篇 antoy sergio
4 篇 chlipala adam
4 篇 felleisen matthi...
4 篇 keller gabriele
4 篇 peyton jones sim...
4 篇 gibbons jeremy
4 篇 morrisett greg
4 篇 findler robert b...
4 篇 walker david
4 篇 krishnaswami nee...
3 篇 flatt matthew
3 篇 mairson harry g.
3 篇 bjerkestrand and...
3 篇 xi hw
3 篇 mcbride conor
3 篇 ohori atsushi

语言

485 篇 英文
2 篇 其他
2 篇 中文

检索条件"任意字段=Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming"

共 489 条记录，以下是11-20 订阅

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

详细简洁

排序：

stableKanren: Integrating Stable Model Semantics with miniKanren 23

stableKanren: Integrating Stable Model Semantics with miniKa...

引用

25th international Symposium on Principles and Practice of Declarative programming (PPDP) As part of the acm sigplan conference on Systems, programming, Languages, and Applications - Software for Humanity (SPLASH)

作者： Guo, Xiangyu Smith, James Bansal, Ajay Arizona State Univ Tempe AZ 85287 USA

ISBN: (纸本)9798400708121

This paper presents stableKanren, a miniKanren extension with normal logic programming support under stable model semantics. MiniKanren is a relational programming solver implemented atop Scheme via shallow embedding, which means the predicate in each rule is encoded as a goal function directly. The solver utilizes the pattern matching macro in Scheme to transform the input goal function and form a static search stream through continuations to achieve the essential features, resolution and unification, in Prolog. However, the static stream only works on monotonic reasoning. Even though the core miniKanren is designed to be easily modified and extended with new features, none of the existing extensions support solving normal logic programs. Also, no normal logic program solvers are based on a functional programming language. We identify and categorize the roles of resolution and unification in top-down solving. And we realize that a dynamic search stream is needed to support non-monotonic reasoning. So we evolve both resolution and unification with new roles, and we exploit the advantages of using macros and continuations further to weave the information generated during runtime into future streams dynamically. We create multiple innovative macros to compile the normal logic program into a program with its complement form, obtain the domain of a variable under different contexts, and generate the new search stream during solving. And we use the coinductive resolution to handle the loop in the normal logic program. In future work, we plan to apply bottom-up optimization to improve our top-down system performance and support various input rules.

关键词： functional programming miniKanren stable model semantics normal logic program solver

来源：评论

学校读者我要写书评

暂无评论

Trieste: A C++ DSL for Flexible Tree Rewriting 17

Trieste: A C++ DSL for Flexible Tree Rewriting

引用

17th acm sigplan international conference on Software Language Engineering, SLE 2024, Co-located with: SPLASH 2024

作者： Clebsch, Sylvan Blomqvist, Matilda Castegren, Elias Johnson, Matthew A. Parkinson, Matthew J. Microsoft Azure Research Austin United States Uppsala University Uppsala Sweden Microsoft Azure Research Cambridge United Kingdom

ISBN: (纸本)9798400711800

Compilation is all about tree rewriting. In functional languages where all data is tree-shaped, tree rewriting is facilitated by pattern matching, but data immutability leads to copying for each update. In object-oriented languages like Java or C++, a standard approach is to use the visitor pattern, which increases modularization but also adds indirection and introduces boilerplate code. In this paper, we introduce Trieste – a novel tree-rewriting DSL, combining the power of C++ with the expressivity of pattern matching. In Trieste, sequences of rewrite passes can be used to read a file to produce an abstract syntax tree (AST), convert from one AST to another, or write an AST to disk. Each pass rewrites an AST in place using subtree pattern matching, where the result is dynamically checked for well-formedness. Checking the well-formedness of trees dynamically enables flexibly changing the tree structure without having to define new data types for each intermediate representation. The well-formedness specification can also be used for scoped name binding and generating random well-formed trees for fuzz testing in addition to checking the shape of trees. Trieste has been used to build fully compliant parsers for YAML and JSON, a transpiler from YAML to JSON, and a compiler and interpreter for the policy language Rego. © 2024 Copyright held by the owner/author(s).

关键词： C++ (programming language)

来源：评论

学校读者我要写书评

暂无评论

Property-Based Testing: Climbing the Stairway to Verification 15

Property-Based Testing: Climbing the Stairway to Verificatio...

引用

15th international conference on Software Language Engineering (SLE)

作者： Chen, Zilin Rizkallah, Christine O'Connor, Liam Susarla, Partha Klein, Gerwin Heiser, Gernot Keller, Gabriele UNSW Sydney Sydney NSW Australia Univ Melbourne Melbourne Vic Australia Univ Edinburgh Edinburgh Midlothian Scotland Proofcraft Sydney NSW Australia Univ Utrecht Utrecht Netherlands

ISBN: (纸本)9781450399197

Property-based testing (PBT) is a powerful tool that is widely available in modern programming languages. It has been used to reduce formal software verification effort. We demonstrate how PBT can be used in conjunction with formal verification to incrementally gain greater assurance in code correctness by integrating PBT into the verification framework of COGENT-a programming language equipped with a certifying compiler for developing high-assurance systems components. Specifically, for PBT and formal verification to work in tandem, we structure the tests to mirror the refinement proof that we used in COGENT's verification framework: The expected behaviour of the system under test is captured by a functional correctness specification, which mimics the formal specification of the system, andwe test the refinement relation between the implementation and the specification. We exhibit the additional benefits that this mutualism brings to developers and demonstrate the techniques we used in this style of PBT, by studying two concrete examples.

关键词： QuickCheck functional programming formal verification systems programming

来源：评论

学校读者我要写书评

暂无评论

Deep Fusion for Efficient Nested Recursive Computations 2022

Deep Fusion for Efficient Nested Recursive Computations

引用

21st acm sigplan international conference on Generative programming: Concepts and Experiences (GPCE)

作者： Shaikhha, Amir Univ Edinburgh Edinburgh Midlothian Scotland

ISBN: (纸本)9781450399203

One of the performance bottlenecks of nested recursive computations is the intermediate collections created at different levels of recursion. The existing techniques such as vertical and horizontal loop fusion do not remove such intermediate allocations. This paper proposes deep fusion, a technique for the efficient compilation of nested recursive computation over collections. The input to our compilation framework is a high-level functional program that can represent computations on flat and nested collections such as lists, sets, bags, and maps. The intermediate collections are removed in three levels. First, the immutable collections are translated into mutable ones by leveraging in-place updates using the destination-passing style technique. Second, deep fusion enables the inner level of recursion to reuse the destinations of the outer levels for in-place updates. Third, deep fusion removes the need to allocate tiny intermediate collections at different depths of recursion. Our experiments show that deep fusion can improve the performance of nested recursion over nested lists and maps.

关键词： Deep Fusion Collection programming Monoid Destination-Passing Style Loop Fusion In-Place Update

来源：评论

学校读者我要写书评

暂无评论

Recursion Synthesis with Unrealizability Witnesses 2022

Recursion Synthesis with Unrealizability Witnesses

引用

43rd acm sigplan international conference on programming Language Design and Implementation (PLDI)

作者： Farzan, Azadeh Lette, Danya Nicolet, Victor Univ Toronto Dept Comp Sci Toronto ON Canada

ISBN: (纸本)9781450392655

We propose SE(2)GIS, a novel inductive recursion synthesis approach with the ability to both synthesize code and declare a problem unsolvable. SE(2)GIS combines a symbolic variant of counterexample-guided inductive synthesis (CEGIS) with a new dual inductive procedure, which focuses on proving a synthesis problem unsolvable rather than finding a solution for it. A vital component of this procedure is a new algorithm that produces a witness, a set of concrete assignments to relevant variables, as a proof that the synthesis instance is not solvable. Witnesses in the dual inductive procedure play the same role that solutions do in classic CEGIS;that is, they ensure progress. Given a reference function, invariants on the input recursive data types, and a target family of recursive functions, SE(2)GIS synthesizes an implementation in this family that is equivalent to the reference implementation, or declares the problem unsolvable and produces a witness for it. We demonstrate that SE(2)GIS is effective in both cases;that is, for interesting data types with complex invariants, it can synthesize non-trivial recursive functions or output witnesses that contain useful feedback for the user.

关键词： Program Synthesis functional programming Invariants Unrealizability Recursion Abstraction

来源：评论

学校读者我要写书评

暂无评论

MimIrADe: Automatic Differentiation in MimIR 25

MimIrADe: Automatic Differentiation in MimIR

引用

34th international conference on Compiler Construction

作者： Ullrich, Marcel Hack, Sebastian Leissa, Roland Saarland Univ Saarland Informat Campus Saarbrucken Germany Univ Mannheim Mannheim Germany

ISBN: (纸本)9798400714078

Automatic differentiation (AD) is at the core of all machine learning frameworks and has applications in scientific computing as well. Theoretical research on reverse-mode AD focuses on functional, higher-order languages, enabling AD to be formulated as a series of local, concise program rewrites. These theoretical approaches focus on correctness but disregard efficiency. Practical implementations, however, employ mutation and taping techniques to enhance efficiency. This approach, however, necessitates intricate, low-level, and non-local program transformations. In this work, we introduce MIMIRADE, a functionally inspired AD technique implemented within a higher-order, graph-based ("sea of nodes") intermediate representation (IR). Our method consists of a streamlined implementation and incorporates standard optimizations, resulting in an efficient AD system. The higher-order nature of the IR enables us to utilize concise functional AD methods, expressing AD through local rewrites. This locality facilitates modular high-level extensions, such as matrix operations, in a straightforward manner. Additionally, the graph-based structure of the IR ensures that critical implementation aspects-particularly the handling of shared pullback invocations-are managed naturally and efficiently. Our AD pass supports a comprehensive set of features, including non-scalar types, pointers, and higher-order recursive functions. We demonstrate through standard benchmarks that a suite of common optimizations effectively eliminates the overhead typically associated with functional AD approaches, producing differentiated code that performs on par with leading mutation and taping techniques. At the same time, MIMIRADE's implementation is an order of magnitude less complex compared to its contenders.

关键词： automatic differentiation functional programming intermediate representation

来源：评论

学校读者我要写书评

暂无评论

Forward Build Systems, Formally 2022

Forward Build Systems, Formally

引用

11th acm sigplan international conference on Certified Programs and Proofs (CPP)

作者： Spall, Sarah Mitchell, Neil Tobin-Hochstadt, Sam Indiana Univ Bloomington IN 47405 USA Meta Worcester Worcs England

ISBN: (纸本)9781450391825

Build systems are a fundamental part of software construction, but their correctness has received comparatively little attention, relative to more prominent parts of the toolchain. In this paper, we address the correctness of forward build systems, which automatically determine the dependency structure of the build, rather than having it specified by the programmer. We first define what it means for a forward build system to be correct-it must behave identically to simply executing the programmer-specified commands in order. Of course, realistic build systems avoid repeated work, stop early when possible, and run commands in parallel, and we prove that these optimizations, as embodied in the recent forward build system RATTLE, preserve our definition of correctness. Along the way, we show that other forward build systems, such as FABRICATE and MEMOIZE, are also correct. We carry out all of our work in Agda, and describe in detail the assumptions underlying both Rattle itself and our modeling of it.

关键词： agda build systems concurrency functional programming program verification systems verified applications

来源：评论

学校读者我要写书评

暂无评论

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.

关键词：

来源：评论

学校读者我要写书评

暂无评论

programming in an fMRI Scanner: A Report from the Field 22

Programming in an fMRI Scanner: A Report from the Field

引用

6th international conference on the Art, Science, and Engineering of programming (programming)

作者： Tanimoto, Steven Thompson, Rob Richards, Todd Yates, Cheri Berninger, Virginia Univ Washington Paul Allen Sch Comp Sci & Eng Seattle WA 98195 USA Colorado Sch Mines Dept Comp Sci Golden CO USA Univ Washington Dept Radiol Seattle WA USA Seattle Childrens Hosp Seattle WA USA Univ Washington Dept Educ Psych Seattle WA USA

ISBN: (纸本)9781450396561

A preliminary study is reported in which six human subjects were scanned while performing a simple form of computer programming. functional magnetic resonance imaging typically precludes the use of ordinary computing equipment due to safety concerns when items with metallic parts are in the scanning room. We used a special visual programming environment, "Kokopelli's World," for which an optics-only trackball was sufficient. This research methodology is described. Aspects of the experience of programming, by one of the authors, in the fMRI scanner are reported. An analysis of the data from the scanning is presented, and brain areas where activity for coding exceeded activity for a control task were identified and are presented here. These observations suggest hypotheses and directions for future research. One hypothesis is that particular aspects of programming are inherently and measurably pleasurable.

关键词： programming fMRI coding in scanner visual language trackball brain imaging brain region Kokopelli's World programming experience scientific poem

来源：评论

学校读者我要写书评

暂无评论

Concurrent and Parallel Garbage Collection for Lightweight Threads on Multicore Processors 2022

Concurrent and Parallel Garbage Collection for Lightweight T...

引用

acm sigplan international conference on Memory Management (ISMM)

作者： Ueno, Katsuhiro Ohori, Atsushi Niigata Univ Niigata Japan Tohoku Univ Sendai Miyagi Japan

ISBN: (纸本)9781450392679

This paper develops a concurrent and parallel garbage collection (GC) method that works with a lightweight thread library realizing the standard M:N threading model. The GC algorithm is organized as a set of procedures that are called from a user-level thread at various occasions and executed in the context of the OS-level threads owning the user-level thread. The procedures realize an on-the-fly collection that does not stop any thread. All OS-level threads cooperatively perform the collection in parallel. This construction achieves the same degree of parallelism as underlying lightweight thread scheduling. We have implemented the algorithm in a Standard ML compiler and have evaluated the performance with sequential and parallel benchmark programs. Our implementation shows good parallel scalability comparable to C programs directly using the lightweight threads library.

关键词： Garbage Collection Lightweight Threads Multicore Processors functional programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共49页 << < 1 2 3 4 5 6 7 8 9 10 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：