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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

7 篇 会议

馆藏范围

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

日期分布

学科分类号

6 篇 工学
- 6 篇 计算机科学与技术...
- 6 篇 软件工程

主题

2 篇 functional progr...
1 篇 agda
1 篇 logic programmin...
1 篇 dependent types
1 篇 probabilistic pr...
1 篇 quantum programm...
1 篇 programming mode...
1 篇 correct-by-const...
1 篇 knowledge repres...

机构

1 篇 univ porto dcc f...
1 篇 delft univ techn...
1 篇 cracs inesc tec ...
1 篇 univ paris cite ...
1 篇 univ paris cite ...
1 篇 univ politecn va...
1 篇 univ kiel inst i...
1 篇 liacc artificial...
1 篇 natl inst adv in...

作者

1 篇 dagand pierre-ev...
1 篇 kesner delia
1 篇 vidal german
1 篇 alves sandra
1 篇 cockx jesper
1 篇 quennet titouan
1 篇 inoue jun
1 篇 hanus michael
1 篇 liesnikov bohdan
1 篇 ramos miguel

语言

7 篇 英文

检索条件"任意字段=22nd Asian Symposium on Programming Languages and Systems, APLAS 2024"

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

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

详细简洁

排序：

22nd asian symposium on programming languages and systems, aplas 2024

22nd Asian Symposium on Programming Languages and Systems, A...

引用

22nd asian symposium on programming languages and systems, aplas 2024

ISBN: (纸本)9789819789429

The proceedings contain 18 papers. The special focus in this conference is on programming languages and systems. The topics include: Random-Access Lists, from EE to FP;generic Reasoning of the Locally Nameless Representation;building a Correct-by-Construction Type Checker for a Dependently Typed Core Language;extending the Quantitative Pattern-Matching Paradigm;hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions;explaining Explanations in Probabilistic Logic programming;quantum programming Without the Quantum Physics;quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers;non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures;type-Based Verification of Connectivity Constraints in Lattice Surgery;on Computational Indistinguishability and Logical Relations;relative Completeness of Incorrectness Separation Logic;OBRA: Oracle-Based, Relational, Algorithmic Type Verification;a Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution;mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem;efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language 22nd

Building a Correct-by-Construction Type Checker for a Depend...

引用

22nd asian symposium on programming languages and systems

作者： Liesnikov, Bohdan Cockx, Jesper Delft Univ Technol Delft Netherlands

ISBN: (纸本)9789819789429;9789819789436

Dependently typed languages allow us to state a program's expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? The goal of this paper is to develop a lightweight technique to improve their trustworthiness by giving a formal specification of the typing rules and intrinsically verifying the type checker with respect to these rules. Concretely, we apply this technique to a subset of Agda's internal language, implemented in Agda. Our development relies on erasure annotations to separate the specification from the runtime of the type checker. We provide guidelines for making design decisions for certified core type checkers and evaluate trade-offs.

关键词： Dependent types Agda Correct-by-Construction programming

来源：评论

学校读者我要写书评

暂无评论

Random-Access Lists, from EE to FP 22nd

Random-Access Lists, from EE to FP

引用

22nd asian symposium on programming languages and systems

作者： Quennet, Titouan Dagand, Pierre-Evariste Univ Paris Cite IRIF CNRS Paris France

ISBN: (纸本)9789819789429;9789819789436

Numerical representations, which were popularized by Okasaki in his seminal book [1], decouple the design of data-types into, first, a choice of a data-structure encoding a suitable numerical system, followed by decorating this structure with as many pieces of data as specified by the underlying numerical system. This paper ambitions to apply McBride's theory of ornaments [2] to explore a structural interpretation of numerical representation. In particular, we propose a journey from Electronic Engineering -computing with binary numbers-to Functional programming -implementing a persistent random-access list datatype.

关键词： Functional programming

来源：评论

学校读者我要写书评

暂无评论

Hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions 22nd

Hybrid Verification of Declarative Programs with Arithmetic ...

引用

22nd asian symposium on programming languages and systems

作者： Hanus, Michael Univ Kiel Inst Informat Kiel Germany

ISBN: (纸本)9789819789429;9789819789436

Functions containing arithmetic operations have often restrictions not expressible by standard type systems of programming languages. The division operation requires that the divisor is non-zero and the factorial function should not be applied to negative numbers. Such partial operations might lead to program crashes if they are applied to unintended arguments. Checking the arguments before each call is tedious and decreases the run-time efficiency. To avoid these disadvantages and support the safe use of partially defined operations, we present an approach to verify the correct use of operations at compile time. To simplify its use, our approach automatically infers non-fail conditions of operations from their definitions and checks whether these conditions are satisfied for all uses of the operations. Arithmetic conditions can be verified by SMT solvers, whereas conditions in operations defined on algebraic data types can be inferred and verified by appropriate type abstractions. Therefore, we present a hybrid method which is applicable to larger programs since only a few arithmetic non-fail conditions need to be checked by an external SMT solver. This approach is implemented for functional logic Curry programs so that it is also usable for purely functional or logic programs.

关键词： Logic programming

来源：评论

学校读者我要写书评

暂无评论

Quantum programming Without the Quantum Physics 22nd

Quantum Programming Without the Quantum Physics

引用

22nd asian symposium on programming languages and systems

作者： Inoue, Jun Natl Inst Adv Ind Sci & Technol 1-8-31 Midorigaoka Ikeda Osaka Japan

ISBN: (纸本)9789819789429;9789819789436

We propose a quantum programming paradigm where all data are familiar classical data, and the only non-classical element is a random number generator that can return results with negative probability. Currently, the vast majority of quantum programming languages instead work with quantum data types made up of qubits. The description of their behavior relies on heavy linear algebra and many interdependent concepts and intuitions from quantum physics, which takes dedicated study to understand. We demonstrate that the proposed view of quantum programming explains its central concepts and constraints in more accessible, computationally relevant terms. This is achieved by systematically reducing everything to the existence of that negative-probability random generator, avoiding mention of advanced physics. This makes quantum programming more accessible to programmers without a deep background in physics or linear algebra. The bulk of this paper is written with such an audience in mind. As a working vehicle, we lay out a simple quantum programming language under this paradigm, showing that not only can it express all quantum algorithms, it also naturally captures the semantics of measurement without ever mentioning qubits or collapse.

关键词： Quantum programming Probabilistic programming programming model

来源：评论

学校读者我要写书评

暂无评论

Explaining Explanations in Probabilistic Logic programming 22nd

Explaining Explanations in Probabilistic Logic Programming

引用

22nd asian symposium on programming languages and systems

作者： Vidal, German Univ Politecn Valencia VRAIN Valencia Spain

ISBN: (纸本)9789819789429;9789819789436

The emergence of tools based on artificial intelligence has also led to the need of producing explanations which are understandable by a human being. In most approaches, the system is considered a black box, making it difficult to generate appropriate explanations. In this work, though, we consider a setting where models are transparent: probabilistic logic programming (PLP), a paradigm that combines logic programming for knowledge representation and probability to model uncertainty. However, given a query, the usual notion of explanation is associated with a set of choices, one for each random variable of the model. Unfortunately, such a set does not explain why the query is true and, in fact, it may contain choices that are actually irrelevant for the considered query. To improve this situation, we present in this paper an approach to explaining explanations which is based on defining a new query-driven inference mechanism for PLP where proofs are labeled with choice expressions, a compact and easy to manipulate representation for sets of choices. The combination of proof trees and choice expressions allows us to produce comprehensible query justifications with a causal structure.

关键词： Knowledge representation

来源：评论

学校读者我要写书评

暂无评论

Extending the Quantitative Pattern-Matching Paradigm 22nd

Extending the Quantitative Pattern-Matching Paradigm

引用

22nd asian symposium on programming languages and systems

作者： Alves, Sandra Kesner, Delia Ramos, Miguel Univ Porto DCC FCUP Fac Sci Porto Portugal CRACS INESC TEC Ctr Adv Comp Syst Porto Portugal Univ Paris Cite CNRS IRIF Paris France LIACC Artificial Intelligence & Comp Sci Lab Porto Portugal

ISBN: (纸本)9789819789429;9789819789436

We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we use a (weak and closed) lambda-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this language not only encodes Plotkin's CBV and CBN lambda-calculus as well as other subsuming frameworks, such as the bang-calculus, but can also be used to interpret the semantics of effectful languages with exceptions. After a thorough study of the untyped language, we introduce a type system based on intersection types, and we show through purely logical methods that the set of terminating terms of the language corresponds exactly to that of well-typed terms. Moreover, by considering non-idempotent intersection types, this characterization turns out to be quantitative, i.e. the size of the type derivation of a term t gives an upper bound for the number of evaluation steps from t to its normal form.

关键词： Functional programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共1页 << < 1 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：