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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

660 篇 会议
97 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

666 篇 工学
- 648 篇 软件工程
- 434 篇 计算机科学与技术...
- 20 篇 控制科学与工程
- 7 篇 信息与通信工程
- 3 篇 材料科学与工程（可...
- 3 篇 电子科学与技术（可...
- 2 篇 光学工程
- 1 篇 机械工程
- 1 篇 仪器科学与技术
- 1 篇 电气工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 化学工程与技术
- 1 篇 农业工程
170 篇 理学
- 167 篇 数学
- 8 篇 统计学（可授理学、...
- 2 篇 物理学
- 2 篇 系统科学
- 1 篇 化学
75 篇 管理学
- 55 篇 管理科学与工程(可...
- 22 篇 图书情报与档案管...
- 4 篇 工商管理
4 篇 法学
- 2 篇 法学
- 2 篇 社会学
1 篇 农学
- 1 篇 作物学

主题

234 篇 languages
153 篇 theory
121 篇 computer program...
106 篇 verification
53 篇 algorithms
48 篇 design
30 篇 computer program...
28 篇 object oriented ...
26 篇 reliability
23 篇 functional progr...
22 篇 high level langu...
22 篇 security
21 篇 performance
19 篇 programming theo...
19 篇 logic programmin...
18 篇 semantics
14 篇 computer systems...
14 篇 type systems
14 篇 concurrency
13 篇 separation logic

机构

15 篇 univ penn philad...
12 篇 carnegie mellon ...
11 篇 univ cambridge c...
11 篇 carnegie mellon ...
8 篇 princeton univ p...
7 篇 microsoft res re...
6 篇 inria rocquencou...
5 篇 inria
5 篇 univ of glasgow ...
5 篇 univ london impe...
5 篇 indiana univ blo...
5 篇 microsoft resear...
5 篇 microsoft resear...
5 篇 tel aviv univ il...
5 篇 university of pe...
5 篇 stanford univ st...
5 篇 univ london impe...
5 篇 cornell univ ith...
5 篇 univ edinburgh e...
4 篇 univ wisconsin m...

作者

11 篇 jones simon peyt...
11 篇 walker david
10 篇 leroy xavier
9 篇 pierce benjamin ...
9 篇 felleisen matthi...
9 篇 harper robert
9 篇 gordon andrew d.
9 篇 abadi martin
8 篇 cardelli luca
7 篇 palsberg jens
7 篇 sagiv mooly
7 篇 calcagno cristia...
7 篇 wadler philip
7 篇 morrisett greg
6 篇 riecke jon g.
6 篇 odersky martin
6 篇 hicks michael
6 篇 fournet cedric
6 篇 kobayashi naoki
5 篇 strub pierre-yve...

语言

690 篇 英文
61 篇 其他
6 篇 中文

检索条件"任意字段=ACM Singplan-sigact Symposium on Principles of Programming Languages"

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

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

详细简洁

排序：

Principal Type Inference for GADTs 16

Principal Type Inference for GADTs

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Chen, Sheng Erwig, Martin UL Lafayette CACS W Lafayette IN USA Oregon State Univ Corvallis OR 97331 USA

ISBN: (纸本)9781450335492

We present a new method for GADT type inference that improves the precision of previous approaches. In particular, our approach accepts more type-correct programs than previous approaches when they do not employ type annotations. A side benefit of our approach is that it can detect a wide range of runtime errors that are missed by previous approaches. Our method is based on the idea to represent type refinements in pattern-matching branches by choice types, which facilitate a separation of the typing and reconciliation phases and thus support case expressions. This idea is formalized in a type system, which is both sound and a conservative extension of the classical Hindley-Milner system. We present the results of an empirical evaluation that compares our algorithm with previous approaches.

关键词： languages Theory Type Inference GADT Choice Type Variational Unification Type Reconciliation

来源：评论

学校读者我要写书评

暂无评论

Conference Record of the Annual acm symposium on principles of programming languages

Conference Record of the Annual ACM Symposium on Principles ...

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages, POPL 2016

ISBN: (纸本)9781450335492

The proceedings contain 61 papers. The topics discussed include: programming the world of uncertain things;type theory in type theory using quotient inductive types;system F-omega with equirecursive types for datatype-generic programming;a theory of effects and resources: adjunction models and polarized calculi;temporal verification of higher-order functional programs;scaling network verification using symmetry and surgery;model checking for symbolic-heap separation logic with inductive predicates;reducing crash recoverability to reachability;query-guided maximum satisfiability;string solving with word equations and transducers: towards a logic for analyzing mutation XSS;symbolic computation of differential equivalences;and unboundedness and downward closures of higher-order pushdown automata.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Fabular: Regression Formulas as Probabilistic programming 16

Fabular: Regression Formulas as Probabilistic Programming

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Borgstrom, Johannes Gordon, Andrew D. Ouyang, Long Russo, Claudio Scibior, Adam Szymczak, Marcin Uppsala Univ S-75105 Uppsala Sweden Microsoft Res Bangalore Karnataka India Univ Edinburgh Edinburgh EH8 9YL Midlothian Scotland Stanford Univ Stanford CA 94305 USA Univ Cambridge Cambridge CB2 1TN England MPI Tubingen Tubingen Germany

ISBN: (纸本)9781450335492

Regression formulas are a domain-specific language adopted by several R packages for describing an important and useful class of statistical models: hierarchical linear regressions. Formulas are succinct, expressive, and clearly popular, so are they a useful addition to probabilistic programming languages? And what do they mean? We propose a core calculus of hierarchical linear regression, in which regression coefficients are themselves defined by nested regressions (unlike in R). We explain how our calculus captures the essence of the formula DSL found in R. We describe the design and implementation of Fabular, a version of the Tabular schema-driven probabilistic programming language, enriched with formulas based on our regression calculus. To the best of our knowledge, this is the first formal description of the core ideas of R's formula notation, the first development of a calculus of regression formulas, and the first demonstration of the benefits of composing regression formulas and latent variables in a probabilistic programming language.

关键词： Bayesian inference linear regression probabilistic programming relational data hierarchical models

来源：评论

学校读者我要写书评

暂无评论

Breaking through the Normalization Barrier: A Self-Interpreter for F-omega 16

Breaking through the Normalization Barrier: A Self-Interpret...

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Brown, Matt Palsberg, Jens Univ Calif Los Angeles Los Angeles CA USA

ISBN: (纸本)9781450335492

According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a self-interpreter for System F-omega, a strongly normalizing lambda-calculus. After a careful analysis of the classical theorem, we show that static type checking in F-omega can exclude the proof's diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in F-omega, including a continuation-passing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.

关键词： languages Theory Lambda Calculus Self Representation Self Interpretation Meta programming

来源：评论

学校读者我要写书评

暂无评论

The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems 16

The Gradualizer: A Methodology and Algorithm for Generating ...

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Cimini, Matteo Siek, Jeremy G. Indiana Univ Bloomington IN 47405 USA

ISBN: (纸本)9781450335492

Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.

关键词： languages Theory gradual typing type systems semantics methodology

来源：评论

学校读者我要写书评

暂无评论

Transforming Spreadsheet Data Types using Examples 16

Transforming Spreadsheet Data Types using Examples

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Singh, Rishabh Gulwani, Sumit Microsoft Res Redmond WA USA

ISBN: (纸本)9781450335492

Cleaning spreadsheet data types is a common problem faced by millions of spreadsheet users. Data types such as date, time, name, and units are ubiquitous in spreadsheets, and cleaning transformations on these data types involve parsing and pretty printing their string representations. This presents many challenges to users because cleaning such data requires some background knowledge about the data itself and moreover this data is typically non-uniform, unstructured, and ambiguous. Spreadsheet systems and programming languages provide some UI-based and programmatic solutions for this problem but they are either insufficient for the user's needs or are beyond their expertise. In this paper, we present a programming by example methodology of cleaning data types that learns the desired transformation from a few input-output examples. We propose a domain specific language with probabilistic semantics that is parameterized with declarative data type definitions. The probabilistic semantics is based on three key aspects: (i) approximate predicate matching, (ii) joint learning of data type interpretation, and (iii) weighted branches. This probabilistic semantics enables the language to handle non-uniform, unstructured, and ambiguous data. We then present a synthesis algorithm that learns the desired program in this language from a set of input-output examples. We have implemented our algorithm as an Excel add-in and present its successful evaluation on 55 benchmark problems obtained from online help forums and Excel product team.

关键词： Algorithms Human Factor Program Synthesis Probabilistic Synthesis Spreadsheet programming programming By Examples Noisy Examples

来源：评论

学校读者我要写书评

暂无评论

Unboundedness and Downward Closures of Higher-Order Pushdown Automata 16

Unboundedness and Downward Closures of Higher-Order Pushdown...

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Hague, Matthew Kochems, Jonathan Ong, C. -H. Luke Univ London Royal Holloway London WC1E 7HU England Univ Oxford Dept Comp Sci Oxford OX1 2JD England

ISBN: (纸本)9781450335492

We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

关键词： Higher-Order Programs Functional Programs Model Checking Verification Formal languages Downward Closures Parikh Images Concurrency Automata Pushdown Automata

来源：评论

学校读者我要写书评

暂无评论

System F-omega with Equirecursive Types for Datatype-Generic programming 16

System F-omega with Equirecursive Types for Datatype-Generic...

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Cai, Yufei Giarrusso, Paolo G. Ostermann, Klaus Univ Tubingen Tubingen Germany

ISBN: (纸本)9781450335492

Traversing an algebraic datatype by hand requires boilerplate code which duplicates the structure of the datatype. Datatype-generic programming (DGP) aims to eliminate such boilerplate code by decomposing algebraic datatypes into type constructor applications from which generic traversals can be synthesized. However, different traversals require different decompositions, which yield isomorphic but unequal types. This hinders the interoperability of different DGP techniques. In this paper, we propose F-omega(mu), an extension of the higher-order polymorphic lambda calculus F-omega with records, variants, and equirecursive types. We prove the soundness of the type system, and show that type checking for first-order recursive types is decidable with a practical type checking algorithm. In our soundness proof we define type equality by interpreting types as infinitary lambda-terms (in particular, Berarducci-trees). To decide type equality we beta-normalize types, and then use an extension of equivalence checking for usual equirecursive types. Thanks to equirecursive types, new decompositions for a datatype can be added modularly and still inter-operate with each other, allowing multiple DGP techniques to work together. We sketch how generic traversals can be synthesized, and apply these components to some examples. Since the set of datatype decomposition becomes extensible, System F-omega(mu) enables using DGP techniques incrementally, instead of planning for them up-front or doing invasive refactoring.

关键词： Datatype-generic programming equirecursive types functors

来源：评论

学校读者我要写书评

暂无评论

Temporal Verification of Higher-Order Functional Programs 16

Temporal Verification of Higher-Order Functional Programs

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Murase, Akihiro Terauchi, Tachio Kobayashi, Naoki Sato, Ryosuke Unno, Hiroshi Nagoya Univ Nagoya Aichi 4648601 Japan JAIST Nagoya Aichi Japan Univ Tokyo Tokyo 1138654 Japan Univ Tsukuba Tsukuba Ibaraki 305 Japan

ISBN: (纸本)9781450335492

We present an automated approach to verifying arbitrary omega regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.

关键词： Algorithms languages Theory Verification Automatic Verification Temporal Properties Higher-Order Programs Automata-Theoretic Verification CEGAR Binary Reachability Analysis

来源：评论

学校读者我要写书评

暂无评论

Example-Directed Synthesis: A Type-Theoretic Interpretation 16

Example-Directed Synthesis: A Type-Theoretic Interpretation

引用

43rd Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Frankle, Jonathan Osera, Peter-Michael Walker, David Zdancewic, Steve Princeton Univ Princeton NJ 08544 USA Grinnell Coll Grinnell IA 50112 USA Univ Penn Philadelphia PA 19104 USA

ISBN: (纸本)9781450335492

Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired adoption in industry, their underlying semantics are less well-understood: what are "examples" and how do they relate to other kinds of specifications? This paper demonstrates that examples can, in general, be interpreted as refinement types. Seen in this light, program synthesis is the task of finding an inhabitant of such a type. This insight provides an immediate semantic interpretation for examples. Moreover, it enables us to exploit decades of research in type theory as well as its correspondence with intuitionistic logic rather than designing ad hoc theoretical frameworks for synthesis from scratch. We put this observation into practice by formalizing synthesis as proof search in a sequent calculus with intersection and union refinements that we prove to be sound with respect to a conventional type system. In addition, we show how to handle negative examples, which arise from user feedback or counterexample-guided loops. This theory serves as the basis for a prototype implementation that extends our core language to support ML-style algebraic data types and structurally inductive functions. Users can also specify synthesis goals using polymorphic refinements and import monomorphic libraries. The prototype serves as a vehicle for empirically evaluating a number of different strategies for resolving the nondeterminism of the sequent calculus bottom-up theorem-proving, term enumeration with refinement type checking, and combinations of both the results of which classify, explain, and validate the design choices of existing synthesis systems. It also provides a platform for measuring the practical value of a specification language that combines "examples" with the more general expressiveness of refinements.

关键词： languages Theory Functional programming Proof Search Sequent Calculus Program Synthesis Type Theory Refinement Types

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：