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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

19 篇 会议

馆藏范围

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

日期分布

学科分类号

17 篇 工学
- 17 篇 计算机科学与技术...
- 17 篇 软件工程
16 篇 理学
- 16 篇 数学

主题

3 篇 abstract interpr...
3 篇 static analysis
2 篇 (constraint) log...
2 篇 program analysis
2 篇 program transfor...
2 篇 logic programmin...
2 篇 assertions
2 篇 prolog
1 篇 program correctn...
1 篇 computer circuit...
1 篇 logic and functi...
1 篇 deriving new the...
1 篇 parallelism
1 篇 program synthesi...
1 篇 run-time checks
1 篇 complexity analy...
1 篇 partial evaluati...
1 篇 higher-order log...
1 篇 program slicing
1 篇 program transfor...

机构

5 篇 imdea software i...
3 篇 spanish council ...
2 篇 roskilde univ ro...
2 篇 univ politecn ma...
1 篇 univ copenhagen ...
1 篇 univ politecn va...
1 篇 polish acad sci ...
1 篇 univ kent sch co...
1 篇 univ oxford oxfo...
1 篇 linkoping univ i...
1 篇 diffblue ltd oxf...
1 篇 univ malaga dept...
1 篇 univ lorraine lo...
1 篇 karlsruhe inst t...
1 篇 univ texas dalla...
1 篇 goethe univ
1 篇 t univ madrid up...
1 篇 univ texas dalla...
1 篇 univ mary washin...
1 篇 univ north texas...

作者

4 篇 hermenegildo man...
4 篇 morales jose f.
2 篇 casso ignacio
2 篇 lopez-garcia ped...
1 篇 kraemer jonas
1 篇 drabent wlodzimi...
1 篇 kirsten michael
1 篇 giacobazzi rober...
1 篇 kesseli pascal
1 篇 orchard dominic
1 篇 gallagher john p...
1 篇 silvan josep
1 篇 kirkeby maja han...
1 篇 schmidt-schauss ...
1 篇 david cristina
1 篇 tarau paul
1 篇 erbatur serdar
1 篇 kroening daniel
1 篇 klemen maximilia...
1 篇 hughes jack

语言

19 篇 英文

检索条件"任意字段=30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020"

共 19 条记录，以下是1-10 订阅

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

详细简洁

排序：

30th international conference on logic-based program synthesis and transformation, lopstr 2020

30th International Conference on Logic-Based Program Synthes...

引用

30th international conference on logic-based program synthesis and transformation, lopstr 2020

ISBN: (纸本)9783030684457

the proceedings contain 17 papers. the special focus in this conference is on logic-based program synthesis and transformation. the topics include: Translation of Interactive Datalog programs for Microcontrollers to Finite State Machines;generating Functions for Probabilistic programs;verification of Multiplayer Stochastic Games via Abstract Dependency Graphs;testing Your (Static Analysis) Truths;slicing Unconditional Jumps with Unnecessary Control Dependencies;a Formal Model for a Linear Time Correctness Condition of Proof Nets of Multiplicative Linear logic;synthesis of Modality Definitions and a theorem Prover for Epistemic Intuitionistic logic;runtime Complexity Analysis of logically Constrained Rewriting;confluence and Commutation for Nominal Rewriting Systems with Atom-Variables;pattern Eliminating transformations;nominal Unification with Letrec and Environment-Variables;terminating Non-disjoint Combined Unification;slepice: Towards a Verified Implementation of Type theory in Type theory;resourceful program synthesis from Graded Linear Types;reasoning in the theory of Heap: Satisfiability and Interpolation.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A Formal Model for a Linear Time Correctness Condition of Proof Nets of Multiplicative Linear logic 30th

A Formal Model for a Linear Time Correctness Condition of Pr...

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Matsuoka, Satoshi Natl Inst Adv Ind Sci & Technol 1-1-1 Umezono Tsukuba Ibaraki 3058561 Japan

ISBN: (纸本)9783030684457;9783030684464

In a previous paper, we have reported a new linear time correctness condition for proof nets of Multiplicative Linear logic without units, where we gave a description of the algorithm in an informal way. In this paper, we give a formal model for the algorithm. Our formal model is based on a finite state transition system with queues as well as union-find trees as data structures. the model has been obtained by trial and error based on a concrete implementation of the algorithm. In addition, the algorithm has a subtle mechanism in order to avoid deadlock. We give an invariant property of the state transition system and it guarantees the deadlock-freedom.

关键词： Computer circuits

来源：评论

学校读者我要写书评

暂无评论

slepice: Towards a Verified Implementation of Type theory in Type theory 30th

slepice: Towards a Verified Implementation of Type Theory in...

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Farka, Frantisek IMDEA Software Inst Madrid Spain

ISBN: (纸本)9783030684457;9783030684464

Dependent types have proven a useful technique for development of verified software. Despite the existence of many systems based in dependent type theory, mostly interactive theorem provers but also programming languages, there is no system that would itself be implemented using dependent types. Recently, a new approach to type inference and term synthesis for type theory with dependent types emerged that separates the process into an analysis phase that is carried out in type theory, and a search phase that is carried out in a logic programming engine. We describe an architecture of type inference and term synthesis engine for a language with dependent types that is based on the new approach and that is feasible to implement using a dependently typed language. We demonstrate the architecture by describing slepice, its particular implementation.

关键词： Dependent types Type inference Horn clause logic Term synthesis Proof-relevant resolution

来源：评论

学校读者我要写书评

暂无评论

synthesis of Modality Definitions and a theorem Prover for Epistemic Intuitionistic logic 30th

Synthesis of Modality Definitions and a Theorem Prover for E...

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Tarau, Paul Univ North Texas Dept Comp Sci & Engn Denton TX 76203 USA

ISBN: (纸本)9783030684457;9783030684464

We propose a mechanism for automating discovery of definitions, that, when added to a logic system for which we have a theorem prover, extends it to support an embedding of a new logic system into it. As a result, the synthesized definitions, when added to the prover, implement a prover for the new logic. As an instance of the proposed mechanism, we derive a Prolog theorem prover for an interesting but unconventional epistemic logic by starting from the sequent calculus G4IP that we extend with operator definitions to obtain an embedding in intuitionistic propositional logic (IPC). With help of a candidate definition formula generator, we discover epistemic operators for which axioms and theorems of Artemov and Protopopescu's Intuitionistic Epistemic logic (IEL) hold and formulas expected to be non-theorems fail. We compare the embedding of IEL in IPC with a similarly discovered successful embedding of Dosen's double negation modality, judged inadequate as an epistemic operator. Finally, we discuss the failure of the necessitation rule for an otherwise successful S4 embedding and share our thoughts about the intuitions explaining these differences between epistemic and alethic modalities in the context of the Brouwer-Heyting-Kolmogorov semantics of intuitionistic reasoning and knowledge acquisition.

关键词： Automatic synthesis of logic systems Deriving new theorem provers via program synthesis Epistemic intuitionistic logic Propositional intuitionistic logic Prolog-based theorem provers Embedding of modal logics into intuitionistic logic

来源：评论

学校读者我要写书评

暂无评论

Resourceful program synthesis from Graded Linear Types 30th

Resourceful Program Synthesis from Graded Linear Types

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Hughes, Jack Orchard, Dominic Univ Kent Sch Comp Canterbury Kent England

ISBN: (纸本)9783030684457;9783030684464

Linear types provide a way to constrain programs by specifying that some values must be used exactly once. Recent work on graded modal types augments and refines this notion, enabling fine-grained, quantitative specification of data use in programs. the information provided by graded modal types appears to be useful for type-directed program synthesis, where these additional constraints can be used to prune the search space of candidate programs. We explore one of the major implementation challenges of a synthesis algorithm in this setting: how does the synthesis algorithm efficiently ensure that resource constraints are satisfied throughout program generation? We provide two solutions to this resource management problem, adapting Hodas and Miller's input-output model of linear context management to a graded modal linear type theory. We evaluate the performance of both approaches via their implementation as a program synthesis tool for the programming language Granule, which provides linear and graded modal typing.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Slicing Unconditional Jumps with Unnecessary Control Dependencies 30th

Slicing Unconditional Jumps with Unnecessary Control Depende...

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Galindo, Carlos Perez, Sergio Silvan, Josep Univ Politecn Valencia VRAIN Canal de Vera S-N Valencia 46022 Spain

ISBN: (纸本)9783030684457;9783030684464

program slicing is an analysis technique that has a wide range of applications, ranging from compilers to clone detection software, and that has been applied to practically all programming languages. Most program slicing techniques are based on a widely extended program representation, the System Dependence Graph (SDG). However, in the presence of unconditional jumps, there exist some situations where most SDG-based slicing techniques are not as accurate as possible, including more code than strictly necessary. In this paper, we identify one of these scenarios, pointing out the cause of the inaccuracy, and describing the initial solution to the problem proposed in the literature, together with an extension, which solves the problem completely. these solutions modify both the SDG generation and the slicing algorithm. Additionally, we propose an alternative solution, that solves the problem by modifying only the SDG generation, leaving the slicing algorithm untouched.

关键词： program analysis program slicing Unconditional jumps

来源：评论

学校读者我要写书评

暂无评论

Terminating Non-disjoint Combined Unification 30th

Terminating Non-disjoint Combined Unification

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Erbatur, Serdar Marshall, Andrew M. Ringeissen, Christophe Univ Texas Dallas Richardson TX 75083 USA Univ Mary Washington Fredericksburg VA USA Univ Lorraine LORIA INRIA CNRS F-54000 Nancy France

ISBN: (纸本)9783030684457;9783030684464

the equational unification problem, where the underlying equational theory may be given as the union of component equational theories, appears often in practice in many fields such as automated reasoning, logic programming, declarative programming, and the formal analysis of security protocols. In this paper, we investigate the unification problem in the non-disjoint union of equational theories via the combination of hierarchical unification procedures. In this context, a unification algorithm known for a base theory is extended with some additional inference rules to take into account the rest of the theory. We present a simple form of hierarchical unification procedure. the approach is particularly well-suited for any theory where a unification procedure can be obtained in a syntactic way using transformation rules to process the axioms of the theory. Hierarchical unification procedures are exemplified with various theories used in protocol analysis. Next, we look at modularity methods for combining theories already using a hierarchical approach. In addition, we consider a new complexity measure that allows us to obtain terminating (combined) hierarchical unification procedures.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Nominal Unification with Letrec and Environment-Variables 30th

Nominal Unification with Letrec and Environment-Variables

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Schmidt-Schauss, Michael Kutz, Yuliya Goethe Univ Frankfurt Germany

ISBN: (纸本)9783030684457;9783030684464

Unification algorithms of nominal expressions with letrec and atom- and expression-variables are already described in the literature. However, only explicit environments could be treated in nominal unification and the use of abstract environments was restricted to nominal matching. this severely restricts the use of algorithms in applications. the following two restrictions permit a step forward and strongly improve the coverage of the application cases: expression- and environment-variables are restricted to occur at most once in the input equations. A terminating and complete nominal unification algorithm is described that computes complete sets of constrained unifiers. Since the set of ground instances of a complete set may be empty due to constraints, we also provide a decision algorithm for inputs which do not contain permutation-variables and show that then nominal unifiability is NP-complete. For input without an occurrence-restriction for expression-variables and w.r.t. garbage-free ground expressions, we sketch an adapted unification algorithm that produces a complete set of unifiers in NP time. For the decision problem we conjecture that it is harder in this case. We believe that lifting the linearity restrictions for environment-variables leads to a prohibitively high computational complexity.

关键词： Nominal unification Letrec-expressions Abstract environments program transformations Automated deduction

来源：评论

学校读者我要写书评

暂无评论

Testing Your (Static Analysis) Truths 30th

Testing Your (Static Analysis) Truths

引用

30th international conference on logic-based program synthesis and transformation (lopstr)

作者： Casso, Ignacio Morales, Jose F. Lopez-Garcia, P. Hermenegildo, Manuel, V IMDEA Software Inst Madrid Spain Univ Politecn Madrid UPM ETSI Informat Madrid Spain Spanish Council Sci Res CSIC Madrid Spain

ISBN: (纸本)9783030684457;9783030684464

Static analysis is nowadays an essential component of many software development toolsets. Despite some notorious successes in the validation of compilers, comparatively little work exists on the systematic validation of static analyzers, whose correctness and reliability is critical if they are to be inserted in production environments. Contributing factors may be the intrinsic difficulty of formally verifying code that is quite complex and of finding suitable oracles for testing it. In this paper, we propose a simple, automatic method for testing abstract interpretation-based static analyzers. Broadly, it consists in checking, over a suite of benchmarks, that the properties inferred statically are satisfied dynamically. the main advantage of our approach is its simplicity, which stems directly from framing it within the Ciao assertion-based validation framework, and its blended static/dynamic assertion checking approach. We show that in this setting, the analysis can be tested with little effort by combining the following components already present in the framework: the static analyzer, the assertion run-time checking mechanism, the random test case generator, and the unit-test framework. Together they compose a tool that can effectively discover and locate errors in the different components of the analysis framework. We apply our approach to test some of CiaoPP's analysis domains over a wide range of programs, successfully finding non-trivial, previously undetected bugs, with a low degree of effort.

关键词： Static analysis Run-time checks Random testing Assertions Abstract interpretation program analysis (Constraint) logic programming

来源：评论

学校读者我要写书评

暂无评论

the Prolog Debugger and Declarative programming 29th

The Prolog Debugger and Declarative Programming

引用

29th international conference on logic-based program synthesis and transformation (lopstr)

作者： Drabent, Wlodzimierz Polish Acad Sci Inst Comp Sci Warsaw Poland Linkoping Univ IDA Linkoping Sweden

ISBN: (纸本)9783030452599;9783030452605

logic programming is a declarative programming paradigm. programming language Prolog makes logic programming possible, at least to a substantial extent. However the Prolog debugger works solely in terms of the operational semantics. So it is incompatible with declarative programming. this report discusses this issue and tries to find how the debugger may be used from the declarative point of view. the results are rather not encouraging. Also, the box model of Byrd, used by the debugger, is explained in terms of SLD-resolution.

关键词： Declarative diagnosis/Algorithmic debugging Prolog Declarative programming program correctness program completeness

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共2页 << < 1 2 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：