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

丛书名： Wrox Programmer to Programmer

2011年

作者： Oliver Sturm

ISBN: (数字)9780470970287

ISBN: (纸本)9780470744581

Take advantage of the growing trend in functional programming.C# is the number-one language used by .NET developers and one of the most popular programming languages in the world. It has many built-in functional programming features, but most are complex and little understood. With the shift to functional programming increasing at a rapid pace, you need to know how to leverage your existing skills to take advantage of this trend. Functional programming in C# leads you along a path that begins with the historic value of functional ideas. Inside, C# MVP and functional programming expert Oliver Sturm explains the details of relevant language features in C# and describes theory and practice of using functional techniques in C#, including currying, partial application, composition, memoization, and monads. Next, he provides practical and versatile examples, which combine approaches to solve problems in several different areas, including complex scenarios like concurrency and high-performance calculation frameworks as well as simpler use cases like Web Services and business logic *** how C# developers can leverage their existing skills to take advantage of functional programmingUses very little math theory and instead focuses on providing solutions to real development problems with functional programming methods, unlike traditional functional programming titlesIncludes examples ranging from simple cases to more complex scenariosLet Functional programming in C# show you how to get in front of the shift toward functional programming.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Automatic music composition using answer set programming

Automatic music composition using answer set programming

引用

24th International Conference on logic programming (ICLP)

作者： Boenn, Georg Brain, Martin De Vos, Marina Ffitch, John Univ Glamorgan Cardiff Sch Creat & Cultural Ind Pontypridd CF37 1DL M Glam Wales Univ Bath Dept Comp Sci Bath BA2 7AY Avon England

Music composition used to be a pen and paper activity. These days music is often composed with the aid of computer software, even to the point where the computer composes parts of the score autonomously. The composition of most styles of music is governed by rules. We show that by approaching the automation, analysis and verification of composition as a knowledge representation task and formalising these rules in a suitable logical language, powerful and expressive intelligent composition tools can be easily built. This application paper describes the use of answer set programming to construct an automated system, named Anton, that can compose melodic, harmonic and rhythmic music, diagnose errors in human compositions and serve as a computer-aided composition tool. The combination of harmonic, rhythmic and melodic composition in a single framework makes Anton unique in the growing area of algorithmic composition. With near real-time composition, Anton reaches the point where it can not only be used as a component in an interactive composition tool but also has the potential for live performances and concerts or automatically generated background music in a variety of applications. With the use of a fully declarative language and an "off-the-shelf" reasoning engine, Anton provides the human composer a tool which is significantly simpler, more compact and more versatile than other existing systems.

关键词： Answer set programming Applications of ASP Music composition Algorithmic composition Harmonic and melodic composition Diagnosis

来源：评论

学校读者我要写书评

暂无评论

Incremental Checking of Well-Founded Recursive Specifications Modulo Axioms 11

Incremental Checking of Well-Founded Recursive Specification...

引用

13th International ACM SIGPLAN Symposium on Principles and practice of Declarative programming

作者： Schernhammer, Felix Meseguer, Jose Vienna Univ Technol Vienna Austria

ISBN: (纸本)9781450307765

We introduce the notion of well-founded recursive order-sorted equational logic (OS) theories modulo axioms. Such theories define functions by well-founded recursion and are inherently terminating. Moreover, for well-founded recursive theories important properties such as confluence and sufficient completeness are modular for so-called fair extensions. This enables us to incrementally check these properties for hierarchies of such theories that occur naturally in modular rule-based functional programs. Well-founded recursive OS theories modulo axioms contain only commutativity and associativity-commutativity axioms. In order to support arbitrary combinations of associativity, commutativity and identity axioms, we show how to eliminate identity and (under certain conditions) associativity (without commutativity) axioms by theory transformations in the last part of the paper.

关键词： Well-founded recursive theory order-sorted rewriting modulo axioms modularity termination confluence sufficient completeness

来源：评论

学校读者我要写书评

暂无评论

How to Make Ad Hoc Proof Automation Less Ad Hoc 11

How to Make Ad Hoc Proof Automation Less Ad Hoc

引用

16th ACM SIGPLAN International Conference on Functional programming (ICFP 11)

作者： Gonthier, Georges Ziliani, Beta Nanevski, Aleksandar Dreyer, Derek Microsoft Res Redmond WA 98052 USA

ISBN: (纸本)9781450308656

Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself. We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

关键词： Interactive theorem proving custom proof automation Coq canonical structures type classes tactics Hoare Type theory

来源：评论

学校读者我要写书评

暂无评论

Noncomputable conditional distributions

Noncomputable conditional distributions

引用

26th Annual IEEE Symposium on logic in Computer Science (LICS)

作者： Ackerman, Nathanael L. Freer, Cameron E. Roy, Daniel M. Harvard Univ Dept Math One Oxford St Cambridge MA 02138 USA Univ Hawaii Manoa Dept Math Honolulu HI 96815 USA MIT Comp Sci & Artificial Intelligence Lab Cambridge MA 02139 USA

ISBN: (纸本)9780769544120

We study the computability of conditional probability, a fundamental notion in probability theory and Bayesian statistics. In the elementary discrete setting, a ratio of probabilities defines conditional probability. In more general settings, conditional probability is defined axiomatically, and the search for more constructive definitions is the subject of a rich literature in probability theory and statistics. However, we show that in general one cannot compute conditional probabilities. Specifically, we construct a pair of computable random variables (X, Y) in the unit interval whose conditional distribution P[Y| X] encodes the halting problem. Nevertheless, probabilistic inference has proven remarkably successful in practice, even in infinite-dimensional continuous settings. We prove several results giving general conditions under which conditional distributions are computable. In the discrete or dominated setting, under suitable computability hypotheses, conditional distributions are computable. Likewise, conditioning is a computable operation in the presence of certain additional structure, such as independent absolutely continuous noise.

关键词： conditional probability computable probability theory probabilistic programming languages real computation

来源：评论

学校读者我要写书评

暂无评论

PPDP'11 - Proceedings of the 2011 Symposium on Principles and practices of Declarative programming

PPDP'11 - Proceedings of the 2011 Symposium on Principles an...

引用

13th International ACM SIGPLAN Symposium on Principles and practice of Declarative programming, PPDP 2011

ISBN: (纸本)9781450307765

The proceedings contain 17 papers. The topics discussed include: the challenges of constraint-based test generation;towards automatic synthesis of software verification tools;incremental checking of well-founded recursive specifications modulo axioms;graph-transformation verification using monadic second-order logic;a modular semantics for higher-order declarative programming with constraints;minimally strict polymorphic functions;protocol analysis in Maude-NPA using unification modulo homomorphic encryption;symbolic analysis of network security policies using rewrite systems;a contextual semantics for concurrent Haskell with futures;maintaining distributed logic programs incrementally;CLP projection for constraint handling rules;dependent session types via intuitionistic linear type theory;linearity and recursion in a typed lambda-calculus;and nested proof search as reduction in the lambda-calculus.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Fundamental Aspects Concerning the Usability Evaluation of Model-Driven Object Oriented programming Approaches in Machine and Plant Automation

Fundamental Aspects Concerning the Usability Evaluation of M...

引用

1st International Conference on Design, User Experience, and Usability (DUXU)/14th International Conference on Human-Computer Interaction (HCI)

作者： Obermeier, Martin Braun, Steven Sommer, Kerstin Vogel-Heuser, Birgit Tech Univ Munich Inst Automat & Informat Syst Mech Engn D-85748 Garching Germany

ISBN: (纸本)9783642217081

Within the world of automation the trend of model-driven object oriented (oo) engineering has brought up fundamental questions about the applicability of these programming paradigms for Programmable logic Controller (PLC) software. The authors present the results of previously conducted experiments on the usability of the classic procedural paradigm (IEC 61131-3) in machine and plant automation compared to model based approaches for PLC programming, in particular Unified Modeling Language (UML) and domain specific modeling languages. Extrapolating these experiments, we propose a way of enhancing usability evaluations by two means: First we present an improved modeling tool. Second, in order to determine the complexity of the tasks required to develop a PLC-program and to create constant boundary conditions for experimental studies, we propose using Hierarchical Task Analysis (HTA) on both model-driven oo and the state of the art programming approach, concerning typical scenarios. Finally the results of our work are discussed.

关键词： Usability PLC-programming model-driven engineering

来源：评论

学校读者我要写书评

暂无评论

programming Languages and Systems - 20th European Symposium on programming, ESOP 2011, Held as Part of the Joint European Conferences on theory and practice of Software, ETAPS 2011, Proceedings

Programming Languages and Systems - 20th European Symposium ...

引用

20th European Symposium on programming, ESOP 2011, Held as Part of the Joint European Conferences on theory and practice of Software, ETAPS 2011

ISBN: (纸本)9783642197178

The proceedings contain 25 papers. The topics discussed include: verified software toolchain;proving isolation properties for software transactional memory;typing copyless message passing;measure transformer semantics for Bayesian machine learning;transfer function synthesis without quantifier elimination;semantics of concurrent revisions;type-based access control in data-centric systems;linear absolute value relation analysis;dataflow analysis for datarace-free programs;compiling information-flow security to minimal trusted computing bases;improving strategies via SMT solving;typing local control and state using flow analysis;barriers in concurrent separation logic;from exponential to polynomial-time security typing via principal types;secure the clones: static enforcement of policies for secure object copying;and a testing theory for a higher-order cryptographic language.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A long tour from theory to practice

引用

INTELLIGENZA ARTIFICIALE 2011年第1期5卷 133-138页

作者： Greco, Sergio Leone, Nicola Palopoli, Luigi Rullo, Pasquale Sacca, Domenico Univ Calabria DEIS Reude Italy Univ Calabria Dip Matemat Reude Italy

In this paper, we describe the research lines in logic programming, carried out in Cosenza over a period of more than twenty years, which have recently produced promising industrial exploitation follow-ups. The research lines have changed over the time but they have kept the initial interest on combining logic programming with databases techniques, that has been continuously renewed to cope with new challenges, in our attempt to use theory to solve practical problems.

关键词： logic programming DATALOG bottom-up execution stable models disjunctive logic programming answer set programming ontology

来源：评论

学校读者我要写书评

暂无评论

Policy Auditing over Incomplete Logs: theory, Implementation and Applications 11

Policy Auditing over Incomplete Logs: Theory, Implementation...

引用

18th ACM Conference on Computer and Communications Security (CCS)

作者： Garg, Deepak Jia, Limin Datta, Anupam Carnegie Mellon Univ Pittsburgh PA 15213 USA

ISBN: (纸本)9781450310758

We present the design, implementation and evaluation of an algorithm that checks audit logs for compliance with privacy and security policies. The algorithm, which we name reduce, addresses two fundamental challenges in compliance checking that arise in practice. First, in order to be applicable to realistic policies, reduce operates on policies expressed in a first-order logic that allows restricted quantification over in finite domains. We build on ideas from logic programming to identify the restricted form of quantified formulas. The logic can, in particular, express all 84 disclosure-related clauses of the HIPAA Privacy Rule, which involve quantification over the in finite set of messages containing personal information. Second, since audit logs are inherently incomplete (they may not contain sufficient information to determine whether a policy is violated or not), reduce proceeds iteratively: in each iteration, it provably checks as much of the policy as possible over the current log and outputs a residual policy that can only be checked when the log is extended with additional information. We prove correctness, termination, time and space complexity results for reduce. We implement reduce and optimize the base implementation using two heuristics for database indexing that are guided by the syntactic structure of policies. The implementation is used to check simulated audit logs for compliance with the HIPAA Privacy Rule. Our experimental results demonstrate that the algorithm is fast enough to be used in practice.

关键词： Audit Formal logic Incomplete logs Privacy policy

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：