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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

146 篇 会议
14 册 图书

馆藏范围

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

日期分布

学科分类号

125 篇 工学
- 124 篇 计算机科学与技术...
- 73 篇 软件工程
- 4 篇 电气工程
- 4 篇 信息与通信工程
- 2 篇 电子科学与技术（可...
- 2 篇 控制科学与工程
- 1 篇 机械工程
- 1 篇 材料科学与工程（可...
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 化学工程与技术
- 1 篇 生物医学工程（可授...
- 1 篇 网络空间安全
38 篇 理学
- 36 篇 数学
- 1 篇 物理学
- 1 篇 化学
- 1 篇 生物学
5 篇 管理学
- 3 篇 图书情报与档案管...
- 2 篇 管理科学与工程(可...
- 1 篇 工商管理
1 篇 医学
- 1 篇 基础医学(可授医学...
- 1 篇 临床医学
- 1 篇 药学(可授医学、理...

主题

37 篇 logic programmin...
11 篇 logics and meani...
9 篇 program transfor...
8 篇 computer circuit...
8 篇 mathematical log...
8 篇 semantics
7 篇 artificial intel...
6 篇 software enginee...
6 篇 programming tech...
6 篇 programming lang...
5 篇 program analysis
4 篇 program synthesi...
4 篇 software enginee...
4 篇 static analysis
4 篇 constraint handl...
3 篇 source-to-source...
2 篇 program debuggin...
2 篇 constraint logic...
2 篇 floating-point n...
2 篇 concurrent const...

机构

4 篇 univ politecn va...
3 篇 katholieke univ ...
3 篇 nagoya inst tech...
3 篇 univ north texas...
2 篇 univ politecn ma...
2 篇 microsoft resear...
2 篇 univ fed rio gra...
2 篇 univ politecn va...
2 篇 katholieke univ ...
2 篇 univ southern de...
2 篇 rhein westfal th...
2 篇 cnr iasi rome
2 篇 univ complutense...
2 篇 tech u madrid sc...
2 篇 imdea software i...
2 篇 univ new mexico ...
2 篇 univ new mexico ...
2 篇 ecole polytech l...
2 篇 univ ulm d-89069...
2 篇 ecole polytech i...

作者

6 篇 vidal german
4 篇 tarau paul
4 篇 schneider-kamp p...
4 篇 silva josep
4 篇 falaschi moreno
4 篇 seki hirohisa
4 篇 abdennadher slim
4 篇 giesl juergen
3 篇 proietti maurizi...
3 篇 de schreye danny
3 篇 leuschel michael
3 篇 lucas salvador
3 篇 meseguer jose
2 篇 puebla german
2 篇 bruynooghe mauri...
2 篇 senni valerio
2 篇 michael hanus
2 篇 gallagher john p...
2 篇 komendantskaya e...
2 篇 sharaf nada

语言

157 篇 英文
3 篇 中文

检索条件"任意字段=17th International Symposium on Logic-Based Program Synthesis and Transformation"

共 160 条记录，以下是131-140 订阅

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

详细简洁

排序：

A Productivity Checker for logic programming 26th

A Productivity Checker for Logic Programming

引用

26th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Komendantskaya, Ekaterina Johann, Patricia Schmidt, Martin Heriot Watt Univ Edinburgh Midlothian Scotland Appalachian State Univ Boone NC 28608 USA Univ Osnabruck Osnabruck Germany

ISBN: (纸本)9783319631394;9783319631387

Automated analysis of recursive derivations in logic programming is known to be a hard problem. Both termination and non-termination are undecidable problems in Turing-complete languages. However, some declarative languages offer a practical work-around for this problem, by making a clear distinction between whether a program is meant to be understood inductively or coinductively. For programs meant to be understood inductively, termination must be guaranteed, whereas for programs meant to be understood coinductively, productive non-termination (or "productivity") must be ensured. In practice, such classification helps to better understand and implement some non-terminating computations. logic programming was one of the first declarative languages to make this distinction: in the 1980's, Lloyd and van Emden's "computations at infinity" captured the big-step operational semantics of derivations that produce infinite terms as answers. In modern terms, computations at infinity describe "global productivity" of computations in logic programming. Most programming languages featuring coinduction also provide an observational, or small-step, notion of productivity as a computational counterpart to global productivity. this kind of productivity is ensured by checking that finite initial fragments of infinite computations can always be observed to produce finite portions of their infinite answer terms. In this paper we introduce a notion of observational productivity for logic programming as an algorithmic approximation of global productivity, give an effective procedure for semi-deciding observational productivity, and offer an implemented automated observational productivity checker for logic programs.

关键词： logic programming Corecursion Coinduction Termination Productivity

来源：评论

学校读者我要写书评

暂无评论

Non-leftmost unfolding in partial evaluation of logic programs with impure predicates

引用

15th international symposium on logic based program synthesis and transformation

作者： Albert, Elvira Puebla, German Gallagher, John P. Univ Complutense Madrid Sch Comp Sci E-28040 Madrid Spain Tech U Madrid Sch Comp Sci Madrid Spain Roskilde Univ Dept Comp Sci DK-4000 Roskilde Denmark

ISBN: (纸本)3540326545

Partial evaluation of logic programs which contain impure predicates poses non-trivial challenges. Impure predicates include those which produce side-effects, raise errors (or exceptions), and those whose truth value varies according to the degree of instantiation of arguments. In particular, non-leftmost unfolding steps can produce incorrect results since the independence of the computation rule no longer holds in the presence of impure predicates. Existing proposals allow non-leftmost unfolding steps, but at the cost of accuracy: bindings and failure are not propagated backwards to predicates which are potentially impure. In this work we propose a partial evaluation scheme which substantially reduces the situations in which such backpropagation has to be avoided. With this aim, our partial evaluator takes into account the information about purity of predicates expressed in terms of assertions. this allows some optimizations which are not feasible using existing partial evaluation techniques. We argue that our proposal goes beyond existing ones in that it is a) accurate, since the classification of pure vs impure is done at the level of atoms instead of predicates, b) extensible, as the information about purity can be added to programs using assertions without having to modify the partial evaluator itself, and c) automatic, since (backwards) analysis can be used to automatically infer the required assertions. Our approach has been implemented in the context of CiaoPP, the abstract interpretation-based preprocessor of the Ciao logic programming system.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Context Generation from Formal Specifications for C Analysis Tools 27th

Context Generation from Formal Specifications for C Analysis...

引用

27th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Alberti, Michele Signoles, Julien TrustInSoft Paris France CEA LIST Software Reliabil & Secur Lab F-91191 Gif Sur Yvette France

ISBN: (纸本)9783319944609;9783319944593

Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function. Such a context initializes the function parameters and global variables to comply with function requirements. However it may be error-prone to write it by hand: the handwritten context might contain bugs or not match the intended specification. A more robust approach is to specify the context in a dedicated specification language, and hold the analysis tools to support it properly. this may mean to put significant development efforts for enhancing the tools, something that is often not feasible if ever possible. this paper presents a way to systematically generate such a context from a formal specification of a C function. this is applied to a subset of the ACSL specification language in order to generate suitable contexts for the abstract interpretation-based value analysis plug-ins of Frama-C, a framework for analysis of code written in C. the idea here presented has been implemented in a new Frama-C plug-in which is currently in use in an operational industrial setting.

关键词： Formal specification Code generation transformation Code analysis Frama-C ACSL

来源：评论

学校读者我要写书评

暂无评论

Functional and Constraint logic programming 1

引用

丛书名： Lecture Notes in Computer Science

1000年

作者： Herbert Kuchen

ISBN: (数字)9783642225314

ISBN: (纸本)9783642225307

this book constitutes the refereed conference proceedings of the 20th international Workshop on Functional and Constraint logic programming, WFLP 2011, held in Odense, Denmark, in July 2011 as Part of the 13th international symposium on Principles and Practice of Declarative programming (PPDP 2011), the 22st international symposium on logic-based program synthesis and transformation (LOPSTR 2011), and the 4th international Workshop on Approaches and Applications of Inductive programming (AAIP 2011). From the 10 papers submitted, 9 were accepted for presentation the proceeding. the papers cover current research in all areas of functional and logic programming as well as the integration of constraint logic and object-oriented programming, and term rewriting.

关键词： logics and Meanings of programs Mathematical logic and Formal Languages programming Languages, Compilers, Interpreters Artificial Intelligence Symbolic and Algebraic Manipulation Computer Imaging, Vision, Pattern Recognition and Graphics

来源：评论

学校读者我要写书评

暂无评论

Static Analysis 1

引用

丛书名： Lecture Notes in Computer Science

1000年

ISBN: (数字)9783540691662

ISBN: (纸本)9783540691631

this book constitutes the refereed proceedings of the 15th international symposium on Static Analysis, SAS 2008, held in Valencia, Spain in July 2008 - co-located with LOPSTR 2008, the international symposium on logic-based program synthesis and transformation, PPDP 2008, the international ACM SIGPLAN symposium on Principles and Practice of Declarative programming, and PLID 2008, the international Workshop on programming Language Interference and Dependence. the 22 revised full papers presented together with two invited lectures were carefully reviewed and selected from 63 submissions. the papers address all aspects of static analysis including abstract domains, abstract interpretation, abstract testing, compiler optimizations, control flow analysis, data flow analysis, model checking, program specialization, security analysis, theoretical analysis frameworks, type based analysis, and verification systems.

关键词： Software Engineering/programming and Operating Systems programming Languages, Compilers, Interpreters logics and Meanings of programs Software Engineering Mathematical logic and Formal Languages programming Techniques

来源：评论

学校读者我要写书评

暂无评论

logic based program synthesis and transformation 1

引用

丛书名： Lecture Notes in Computer Science

1000年

作者： Maurice Bruynooghe

ISBN: (数字)9783540259381

ISBN: (纸本)9783540221746

this volume contains selected papers from LOPSTR 2003, the 13th Inter- tional symposium on logic-based program synthesis and transformation. the LOPSTR series is devoted to research in logic-based program development. P- ticular topics of interest are speci?cation, synthesis, veri?cation, transformation, specialization, analysis, optimization, composition, reuse, component-based so- ware development, agent-based software development, software architectures, design patterns and frameworks, program re?nement and logics for re?nement, proofs as programs, and applications and tools. LOPSTR 2003 took place at the University of Uppsala from August 25 to August 27 as part of PLI 2003 (Principles, logics, and Implementations of High- Level programming Languages). PLI was an ACM-organized confederation of conferences and workshops with ICFP 2003 (ACM-SIGPLAN international C- ference on Functional programming) and PPDP 2003 (ACM-SIGPLAN Inter- tional Conference on Principles and Practice of Declarative programming) as the main events. the LOPSTR community pro?ted from the shared lectures of the invited speakers, and the active scienti?c discussions enabled by the co-location. LOPSTR 2003 was the thirteenth in a series of events. Past events were held in Manchester, UK (1991, 1992, 1998), Louvain-la-Neuve, Belgium (1993), Pisa, Italy (1994), Arnhem, the Netherlands (1995), Stockholm, Sweden (1996), L- ven, Belgium (1997), Venice, Italy (1999), London, UK (2000), Paphos, Cyprus (2001), and Madrid, Spain (2002).

关键词： Software Engineering/programming and Operating Systems logics and Meanings of programs programming Techniques Mathematical logic and Formal Languages Artificial Intelligence

来源：评论

学校读者我要写书评

暂无评论

Slicing Concurrent Constraint programs 26th

Slicing Concurrent Constraint Programs

引用

26th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Falaschi, Moreno Gabbrielli, Maurizio Olarte, Carlos Palamidessi, Catuscia Univ Siena Dipartimento Ingn Informaz & Sci Matemat Siena Italy Univ Bologna Dipartimento Informat Sci & Ingn Bologna Italy Univ Fed Rio Grande do Norte ECT Natal RN Brazil Ecole Polytech INRIA Palaiseau France Ecole Polytech LIX Palaiseau France

ISBN: (纸本)9783319631394;9783319631387

Concurrent Constraint programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to timed variants of CCP. We also develop a prototypical implementation freely available for making experiments.

关键词： Concurrent Constraint programming program slicing Debugging

来源：评论

学校读者我要写书评

暂无评论

the next 700 synthesis calculi 11

The next 700 synthesis calculi

引用

11th international symposium of Formal Methods Europe, FME 2002

作者： Basin, David Universität Freiburg Freiburg Germany

ISBN: (纸本)9783540439288

Over the last decade I have worked with colleagues on different projects to develop, implement, and automate the use of calculi for program synthesis and transformation. these projects had different motivations and goals and differed too in the kinds of programs synthesized (e.g., functional programs, logic programs, and even circuit descriptions). However, despite their differences they were all based on three simple ideas. First, calculi can be formally derived in a rich enough logic (e.g., higher-order logic). Second, higher-order resolution is the central mechanism used to synthesize programs during proofs of their correctness. And third, synthesis proofs have a predictable form and can be partially or completely automated. In the talk I explain these ideas and illustrate the general methodology employed. © Springer-Verlag Berlin Heidelberg 2002.

关键词： Biomineralization

来源：评论

学校读者我要写书评

暂无评论

the program inverter LRinv and its structure

引用

7th international symposium on Practical Aspects of Declarative Languages (PADL)

作者： Kawabe, M Glück, R Waseda Univ Grad Sch Sci & Engn Tokyo 1698555 Japan Univ Copenhagen DIKU Dept Comp Sci DK-2100 Copenhagen Denmark

ISBN: (纸本)3540243623

program inversion is a fundamental concept in program transformation. We describe the principles behind an automatic program inverter, which we developed for a first-order functional language, and show several inverse programs automatically produced by our system. the examples belong to different application areas, including encoding and decoding, printing and parsing, and bidirectional data conversion. the core of the system uses a stack-based language, local inversion, and eliminates nondeterminism by applying methods from parsing theory.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

Latte: Locality Aware transformation for High-Level synthesis 26

Latte: Locality Aware Transformation for High-Level Synthesi...

引用

26th IEEE Annual international symposium on Field-programmable Custom Computing Machines (FCCM)

作者： Cong, Jason Wei, Peng Yu, Cody Hao Zhou, Peipei Univ Calif Los Angeles Comp Sci Los Angeles CA 90095 USA

ISBN: (纸本)9781538655221

In this paper we classify the timing degradation problems using four common collective communication and computation patterns in HLS-based accelerator design: scatter, gather, broadcast and reduce. these widely used patterns scale poorly in one-to-all or all-to-one data movements between off-chip communication interface and on-chip storage, or inside the computation logic. therefore, we propose the Latte microarchitecture featuring pipelined transfer controllers (PTC) along data paths in these patterns. Furthermore, we implement an automated framework to apply our Latte implementation in HLS with minimal user efforts. Our experiments show that Latte-optimized designs greatly improve the timing of baseline HLS designs by 1.50x with only 3.2% LUT overhead on average, and 2.66x with 2.7% overhead at maximum.

关键词： Microarchitecture Delays Wires System-on-chip Pipelines Layout Tools"

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共16页 << < 7 8 9 10 11 12 13 14 15 16 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：