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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

11 篇 会议

馆藏范围

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

日期分布

学科分类号

10 篇 工学
- 10 篇 计算机科学与技术...
- 8 篇 软件工程
- 1 篇 力学（可授工学、理...
- 1 篇 材料科学与工程（可...
- 1 篇 信息与通信工程
- 1 篇 建筑学
- 1 篇 化学工程与技术
- 1 篇 农业工程
3 篇 理学
- 2 篇 数学
- 1 篇 物理学
- 1 篇 化学
- 1 篇 生物学
1 篇 农学
- 1 篇 作物学
1 篇 管理学
- 1 篇 图书情报与档案管...

主题

2 篇 formal languages
2 篇 functional progr...
1 篇 computer circuit...
1 篇 iterative method...
1 篇 errors
1 篇 program compiler...
1 篇 abstracting
1 篇 differentiation ...
1 篇 transducers

机构

7 篇 functional progr...
3 篇 functional progr...
1 篇 department of co...
1 篇 functional progr...
1 篇 institut de rech...
1 篇 institut fur inf...
1 篇 department of co...
1 篇 dfg research tra...

作者

3 篇 day laurence e.
3 篇 nilsson henrik
2 篇 van gijzel bas
2 篇 hutton graham
1 篇 kraus nicolai
1 篇 ahrens benedikt
1 篇 rypáček ondřej
1 篇 spadotti régis
1 篇 bahr patrick
1 篇 legatiuk dmitrii
1 篇 altenkirch thors...
1 篇 sestini filippo
1 篇 abel andreas
1 篇 capriotti paolo
1 篇 giorgidze george

语言

11 篇 英文

检索条件"机构=Functional Programming Laboratory"

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

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

详细简洁

排序：

Normalization by evaluation for typed weak λ-reduction 24

Normalization by evaluation for typed weak λ-reduction

引用

24th International Conference on Types for Proofs and Programs, TYPES 2018

作者： Sestini, Filippo Functional Programming Laboratory University of Nottingham United Kingdom

ISBN: (纸本)9783959771061

Weak reduction relations in the λ-calculus are characterized by the rejection of the so-called ξ-rule, which allows arbitrary reductions under abstractions. A notable instance of weak reduction can be found in the literature under the name restricted reduction or weak λ-reduction. In this work, we attack the problem of algorithmically computing normal forms for λwk, the λ-calculus with weak λ-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute λwk-normal forms. We observe that some aspects of weak λ-reduction prevent us from normalizing λwk directly, thus devise a new, better-behaved weak calculus λex, and reduce the normalization problem for λw to that of λex. We finally define type systems for both calculi and apply Normalization by Evaluation to λex, obtaining a normalization proof for λwk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory. © Filippo Sestini;licensed under Creative Commons License CC-BY

关键词： Differentiation (calculus)

来源：评论

学校读者我要写书评

暂无评论

Compilation à la Carte 13

Compilation à la Carte

引用

25th International Symposium on Implementation and Application of functional Languages, IFL 2013

作者： Day, Laurence E. Hutton, Graham Functional Programming Laboratory University of Nottingham United Kingdom

ISBN: (纸本)9781450329880

In previous work, we proposed a new approach to the problem of implementing compilers in a modular manner, by combining earlier work on the development of modular interpreters using monad transformers with the à la carte approach to modular syntax. In this article, we refine and extend our existing framework in a number of directions. In particular, we show how generalised algebraic datatypes can be used to support a more modular approach to typing individual language features, we increase the expressive power of the framework by considering mutable state, variable binding, and the issue of noncommutative effects, and we show how the Zinc Abstract Machine can be adapted to provide a modular universal target machine for our modular compilers. Copyright © 2013 ACM.

关键词： Abstracting

来源：评论

学校读者我要写书评

暂无评论

Tools for the implementation of argumentation models

Tools for the implementation of argumentation models

引用

3rd Imperial College Computing Student Workshop, ICCSW 2013

作者： Van Gijzel, Bas Functional Programming Laboratory School of Computer Science University of Nottingham United Kingdom

ISBN: (纸本)9783939897637

The structured approach to argumentation has seen a surge of models, introducing a multitude of ways to deal with the formalisation of arguments. However, while the development of the mathematical models have flourished, the actual implementations and development of methods for implementation of these models have been lagging behind. This paper attempts to alleviate this problem by providing methods that simplify implementation, i.e. we demonstrate how the functional programming language Haskell can naturally express mathematical definitions and sketch how a theorem prover can verify this implementation. Furthermore, we provide methods to streamline the documenting of code, showing how literate programming allows the implementer to write formal definition, implementation and documentation in one file. All code has been made publicly available and reusable.

关键词： functional programming

来源：评论

学校读者我要写书评

暂无评论

Towards modular compilers for effects 12th

Towards modular compilers for effects

引用

12th International Symposium on Trends in functional programming, TFP 2011

作者： Day, Laurence E. Hutton, Graham Functional Programming Laboratory School of Computer Science University of Nottingham United Kingdom

ISBN: (纸本)9783642320361

Compilers are traditionally factorised into a number of separate phases, such as parsing, type checking, code generation, etc. However, there is another potential factorisation that has received comparatively little attention: the treatment of separate language features, such as mutable state, input/output, exceptions, concurrency and so forth. In this article we focus on the problem of modular compilation, in which the aim is to develop compilers for separate language features independently, which can then be combined as required. We summarise our progress to date, issues that have arisen, and further work. © Springer-Verlag Berlin Heidelberg 2012.

关键词： Program compilers

来源：评论

学校读者我要写书评

暂无评论

Haskell gets argumentative

Haskell gets argumentative

引用

13th Symposium on Trends in functional programming, TFP 2012

作者： Van Gijzel, Bas Nilsson, Henrik Functional Programming Laboratory School of Computer Science University of Nottingham United Kingdom

ISBN: (纸本)9783642404467

Argumentation theory is an interdisciplinary field studying how conclusions can be reached through logical reasoning. The notion of argument is completely general, including for example legal arguments, scientific arguments, and political arguments. Computational argumentation theory is studied in the context of artificial intelligence, and a number of computational argumentation frameworks have been put forward to date. However, there is a lack of concrete, high level realisations of these frameworks, which hampers research and applications at a number of levels. We hypothesise that the lack of suitable domain-specific languages in which to formalise argumentation frameworks is a contributing factor. In this paper, we present a formalisation of a particular computational argumentation framework, Carneades, as a case study with a view to investigate the extent to which functional languages are useful as a means to realising computational argumentation frameworks and reason about them. © 2013 Springer-Verlag.

关键词： functional programming

来源：评论

学校读者我要写书评

暂无评论

Mixed-level embedding and JIT compilation for an iteratively staged DSL

Mixed-level embedding and JIT compilation for an iteratively...

引用

Lecture Notes in Computer Science

作者： Giorgidze, George Nilsson, Henrik Functional Programming Laboratory School of Computer Science University of Nottingham United Kingdom

ISBN: (纸本)9783642207747

This paper explores how to implement an iteratively staged domain-specific language (DSL) by embedding into a functional language. The domain is modelling and simulation of physical systems where models are expressed in terms of non-causal differential-algebraic equations;i.e., sets of constraints solved through numerical simulation. What distinguishes our language is that the equational constraints are first class entities allowing for an evolving model structure characterised by repeated generation of updated constraints. Hence iteratively staged. Our DSL can thus be seen as a combined functional and constraint programming language, albeit a two-level one, with the functional language chiefly serving as a meta language. However, the two levels do interact throughout the simulation. The embedding strategy we pursue is a mixture of deep and shallow, with the deep embedding enabling just-in-time (JIT) compilation of the constraints as they are generated for efficiency, while the shallow embedding is used for the remainder for maximum leverage of the host language. The paper is organised around a specific DSL, but our implementation strategy should be applicable for iteratively staged languages in general. Our DSL itself is further a novel variation of a declarative constraint programming language. © 2011 Springer-Verlag.

关键词： Iterative methods

来源：评论

学校读者我要写书评

暂无评论

programming macro tree transducers

Programming macro tree transducers

引用

2013 9th ACM SIGPLAN Workshop on Generic programming, WGP 2013 - Co-located with the 18th ACM SIGPLAN International Conference on functional programming, ICFP 2013

作者： Bahr, Patrick Day, Laurence E. Department of Computer Science University of Copenhagen Denmark Functional Programming Laboratory University of Nottingham United Kingdom

ISBN: (纸本)9781450323895

A tree transducer is a set of mutually recursive functions transforming an input tree into an output tree. Macro tree transducers extend this recursion scheme by allowing each function to be defined in terms of an arbitrary number of accumulation parameters. In this paper, we show how macro tree transducers can be concisely represented in Haskell, and demonstrate the benefits of utilising such an approach with a number of examples. In particular, tree transducers afford a modular programming style as they can be easily composed and manipulated. Our Haskell representation generalises the original definition of (macro) tree transducers, abolishing a restriction on finite state spaces. However, as we demonstrate, this generalisation does not affect compositionality.

关键词： Transducers

来源：评论

学校读者我要写书评

暂无评论

A syntactical approach to weak ω-Groupoids

A syntactical approach to weak ω-Groupoids

引用

26th International Workshop on Computer Science Logic, CSL 2012/21st Annual Conference of the European Association for Computer Science Logic, EACSL

作者： Altenkirch, Thorsten Rypáček, Ondřej Functional Programming Laboratory School of Computer Science University of Nottingham United Kingdom Department of Computer Science University of Sheffield United Kingdom

ISBN: (纸本)9783939897422

When moving to a Type Theory without proof-irrelevance the notion of a setoid has to be generalized to the notion of a weak ω-groupoid. As a first step in this direction we study the formalisation of weak ω-groupoids in Type Theory. This is motivated by Voevodsky's proposal of univalent type theory which is incompatible with proof-irrelevance and the results by Lumsdaine and Garner/van de Berg showing that the standard eliminator for equality gives rise to a weak ω-groupoid. © Thorsten Altenkirch and Ondřej Rypáček.

关键词： Formal languages

来源：评论

学校读者我要写书评

暂无评论

Abstract modelling: Towards a typed declarative language for the conceptual modelling phase 17

Abstract modelling: Towards a typed declarative language for...

引用

8th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools, EOOLT 2017

作者： Legatiuk, Dmitrii Nilsson, Henrik DFG Research Training Group 1462 Bauhaus-Universität Weimar Weimar Germany Functional Programming Laboratory School of Computer Science University of Nottingham United Kingdom

ISBN: (纸本)9781450363730

The growing complexity of modern engineering tasks necessitates improved tool support for modelling, in particular tools allowing early detection of modelling errors. Broadly, there are two classes of modelling errors: (i) errors related to abstract modelling, e.g. conceptual errors concerning the coherence of a model as a whole, and (ii) errors related to concrete modelling, e.g. questions of approximation quality and implementation. Concrete modelling errors are relatively well understood, but abstract modelling errors less so. If, however, abstract modelling errors could be detected early, before concrete implementation starts, this would be very beneficial. Unfortunately, existing engineering tools, like current modelling languages, do not support modelling in the abstract well, leaving a gap in the engineering tool chain. To overcome this problem, this paper presents a first step towards a language supporting abstract modelling in mathematical physics with the aim of ensuring coherence of coupled multiphysics models early in the design process. To that end, following the approach of functional Hybrid Modelling, we discuss how a language supporting quite general modelling equations can be realised as an embedding in Haskell. The appeal of the approach is that only few core concepts are needed, simplifying the semantics, and that much of the language infrastructure comes for free thanks to embedding. © 2017 Copyright held by the owner/author(s).

关键词： Errors

来源：评论

学校读者我要写书评

暂无评论

Non-wellfounded trees in homotopy type theory 13

Non-wellfounded trees in homotopy type theory

引用

13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015

作者： Ahrens, Benedikt Capriotti, Paolo Spadotti, Régis Institut de Recherche en Informatique de Toulouse Université Paul Sabatier Toulouse France Functional Programming Laboratory School of Computer Science University of Nottingham United Kingdom

ISBN: (纸本)9783939897873

We prove a conjecture about the constructibility of coinductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable. Indeed, in this work, we construct coinductive types in a subsystem of Homotopy Type Theory;this subsystem is given by Intensional Martin- Löf type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda. © Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti;.

关键词： Formal languages

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共2页 << < 1 2 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：