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

INFORMATION SYSTEMS 2009年第7期34卷 624-642页

作者： Reichenbach, Christoph Burke, Michael G. Peshansky, Igor Raghavachari, Mukund IBM Corp TJ Watson Res Ctr Armonk NY USA Univ Colorado Boulder CO 80309 USA

The widespread adoption of XML has led to programming languages that support XML as a first class construct. In this paper, we present a method for analyzing and optimizing imperative XML processing programs. In particular, we present a program analysis, based on a flow-sensitive type system, for detecting both redundant computations and redundant traversals in such programs. The analysis handles imperative loops that traverse XML values explicitly and declarative queries over XML data in a uniform framework. We describe two optimizations that take advantage of our analysis: one merges queries that traverse the same set of XML nodes, and the other replaces an XPath expression by a previously computed result. We demonstrate performance improvements for selected XMark benchmark queries and XLinq sample queries. (C) 2009 Elsevier B.V. All rights reserved.

关键词： Program analysis XML imperative programming

来源：评论

学校读者我要写书评

暂无评论

Finitism, imperative programs and primitive recursion

引用

JOURNAL OF LOGIC AND COMPUTATION 2021年第1期31卷 179-192页

作者： Leivant, Daniel Indiana Univ SICE Bloomington IN 47405 USA Univ Paris Diderot IRIF Paris France

Following the Crisis of Foundations Hilbert proposed to consider a finitistic form of arithmetic as mathematics' safe core. This approach to finitism has often admitted primitive recursive function definitions as obviously finitistic, but some have advocated the inclusion of additional variants of recurrence, while others argued that, to the contrary, primitive recursion exceeds finitism. In a landmark essay, William Tait contested the finitistic nature of these extensions, due to their impredicativity, and advocated identifying finitism with primitive recursive arithmetic, a stance often referred to as Tait's Thesis. However, a problem with Tait's argument is that the recurrence schema has itself impredicative and non-finitistic facets, starting with an explicit reference to the functions being defined, which are after all infinite objects. It is therefore desirable to buttress Tait's Thesis on grounds that avoid altogether any trace of concrete infinities or impredicativity. We propose here to do just that, building on the generic framework of [13]. We provide further evidence for Tait's Thesis by outlining a proof of a purely finitistic version of Parsons' theorem, whose intuitive gist is that finitistic reasoning is equivalent to finitistic computing.

关键词： Finitism primitive recursive arithmetic finite partial functions primitive recursive functions imperative programming loop variant Parsons' theorem

来源：评论

学校读者我要写书评

暂无评论

USING PROCEDURAL PARAMETERS AND CONTINUATIONS IN COMBINATORIAL SEARCHES

引用

SOFTWARE-PRACTICE & EXPERIENCE 1994年第4期24卷 377-386页

作者： HWANG, WP WANG, CL TAMKANG UNIV DEPT COMP & INFORMAT ENGNTAIPEITAIWAN

We use procedural parameters as a means to cut off unwanted branches in a search tree. The technique may be used to effect non-blind backtracking. A recursive algorithm for generating all strings of n pairs of balanced parentheses is chosen as an illustrative example, since it cannot be formulated by conventional recursive backtracking.

关键词： imperative programming PROCEDURAL PARAMETERS CONTINUATIONS PASCAL

来源：评论

学校读者我要写书评

暂无评论

NixOS: A purely functional Linux distribution

引用

JOURNAL OF FUNCTIONAL programming 2010年第5-6期20卷 577-615页

作者： Dolstra, Eelco Loh, Andres Pierron, Nicolas Delft Univ Technol Dept Software Technol NL-2600 GA Delft Netherlands Univ Utrecht Dept Informat & Comp Sci NL-3508 TB Utrecht Netherlands EPITA Res & Dev Lab F-94276 Le Kremlin Bicetre France

Existing package and system configuration management tools suffer from an imperative model, where system administration actions such as package upgrades or changes to system configuration files are stateful: they destructively update the state of the system. This leads to many problems, such as the inability to roll back changes easily, to deploy multiple versions of a package side-by-side, to reproduce a configuration deterministically on another machine, or to reliably upgrade a system. In this paper we show that we can overcome these problems by moving to a purely functional system configuration model. This means that all static parts of a system (such as software packages, configuration files and system startup scripts) are built by pure functions and are immutable, stored in a way analogous to a heap in a purely functional language. We have implemented this model in NixOS, a non-trivial Linux distribution that uses the Nix package manager to build the entire system configuration from a modular, purely functional specification.

关键词： LINUX operating systems ELECTRONIC systems SOFTWARE configuration management imperative programming COMPUTER software

来源：评论

学校读者我要写书评

暂无评论

An observationally complete program logic for imperative higher-order functions

引用

THEORETICAL COMPUTER SCIENCE 2014年 517卷 75-101页

作者： Honda, Kohei Yoshida, Nobuko Berger, Martin Univ London Dept Comp Sci London WC1E 7HU England Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2AZ England Univ Sussex Dept Informat Brighton BN1 9RH E Sussex England

We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Completeness Characteristic formulae Program logic Higher-order function imperative programming Observational equivalence

来源：评论

学校读者我要写书评

暂无评论

Inference of Session Types From Control Flow

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2010年第6期238卷 15-40页

作者： Collingbourne, Peter Kelly, Paul H. J. Imperial Coll London Dept Comp London SW7 2AZ England

This is a study of a technique for deriving the session type of a program written in a statically typed imperative language from its control flow. We impose on our unlabelled session type syntax a well-formedness constraint based upon normalisation and explore the effects thereof. We present our inference algorithm declaratively and in a form suitable for implementation, and illustrate it with examples. We then present an implementation of the algorithm using a program analysis and transformation toolkit.

关键词： Session types imperative programming control flow type inference program analysis

来源：评论

学校读者我要写书评

暂无评论

Computation for Architecture, hybrid visual and textual language: Research developments and considerations about the implementation of structural imperative and object-oriented paradigms

引用

INTERNATIONAL JOURNAL OF ARCHITECTURAL COMPUTING 2022年第3期20卷 673-687页

作者： Henriques, Goncalo Castro Xavier, Pedro Maciel Silva, Victor de Luca Bispo, Luca Redua Fraga, Joao Victor Univ Fed Rio de Janeiro Rio De Janeiro RJ Brazil Univ Fed Rio de Janeiro Engn Comp & Informacao Escola Politecn Rio De Janeiro RJ Brazil Univ Fed Rio de Janeiro Engn Controle & Automacao Escola Politecn Rio De Janeiro RJ Brazil

In the fourth industrial revolution, programming promises to be a fundamental subject like mathematics, science, languages or the arts. Architects design more than buildings developing innovative methods and they are among the pioneers in visual programming development. However, after more than 10 years of visual programming in architecture, despite the fast-learning curve, visual programming presents considerable limitations to solve complex problems. To overcome limitations, the authors propose to associate the advantages of visual and textual languages in Python. The article addresses an ongoing research study to implement Computational Methods in Architectural Education. The authors began by describing the general goal of this project, and of this article in particular. This article focuses on the implementation of two disciplines 'Computation for Architecture in Python' I and II. The first discipline uses programming based on the construction of functions in the imperative language, implemented in the text editor, in visual programming, using Grasshopper methods. The second discipline, which is under development, intends to teach object-oriented programming. The results of the first discipline are encouraging;despite reported difficulties in programming fundamentals, such as lists, loops and recursion. The development of the second discipline, in object-oriented programming, deals with the concepts of classes and objects, and more abstract principles such abstraction, inheritance, polymorphism or encapsulation. This paradigm allows building robust programs, but requires a more in-depth syntax. The article reports this ongoing research on this new paradigm of object-oriented language, expanding the application of a hybrid visual-textual language in Architecture.

关键词： computation textual programming visual programming imperative programming object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Trace-based verification of imperative programs with I/O

引用

JOURNAL OF SYMBOLIC COMPUTATION 2011年第2期46卷 95-118页

作者： Malecha, Gregory Morrisett, Greg Wisnesky, Ryan Harvard Univ Cambridge MA 02138 USA

In this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers, files, and socket I/O with respect to high level I/O protocol descriptions by using the Coq proof assistant. We present a web-based course gradebook application developed with Ynot, a Coq library for verified imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynot's underlying Hoare logic with event traces to reason about I/O and protocol behavior. Expressive abstractions allow the modular verification of both high level specifications like privacy guarantees and low level properties like data structure pointer invariants. (C) 2010 Elsevier Ltd. All rights reserved.

关键词： Program verification Separation logic Dependent types Traces imperative programming Ynot

来源：评论

学校读者我要写书评

暂无评论

Teaching programming broadly and deeply: The Kernel language approach

Teaching programming broadly and deeply: The Kernel language...

引用

Conference on Informatics Curricula, Teaching Methods and Best Practice

作者： Van Roy, P Haridi, S Univ Catholique Louvain Dept Comp Sci & Engn INGI B-1348 Louvain Belgium

ISBN: (纸本)140207266X

We present the kernel language approach;a new way to teach programming that situates most of the widely known programming paradigms (including imperative, object-oriented, concurrent, logic, and functional) into a uniform setting that shows their deep relationships and how to use them together. Widely different practical languages (exemplified by Java, Haskell, Prolog, and Erlang) with their rich panoplies of abstractions and syntax are explained by straightforward translations into closely related kernel languages, simple languages that consist of small numbers of programmer-significant concepts. Kernel languages are easy to understand and have a simple formal semantics that can be used by practicing programmers to reason about correctness and complexity.

关键词： computer programming education curriculum science engineering programming concepts programming paradigms kernel language dataflow concurrency functional programming object-oriented programming logic programming imperative programming programming techniques

来源：评论

学校读者我要写书评

暂无评论

imperative abstractions for functional actions

引用

JOURNAL OF LOGIC AND ALGEBRAIC programming 2010年第8期79卷 768-793页

作者： Guttmann, Walter Univ Ulm Inst Programmiermethod & Compilerbau D-89069 Ulm Germany

We elaborate our relational model of non-strict, imperative computations. The theory is extended to support infinite data structures. To facilitate their use in programs, we extend the programming language by concepts such as procedures, parameters, partial application, algebraic data types, pattern matching and list comprehensions. For each concept, we provide a relational semantics. Abstraction is further improved by programming patterns such as fold, unfold and divide-and-conquer. To support program reasoning, we prove laws such as fold-map fusion, otherwise known from functional programming languages. We give examples to show the use of our concepts in programs. (C) 2010 Elsevier Inc. All rights reserved.

关键词： Fold Higher-order procedures imperative programming Infinite data structures Lazy evaluation Non-strictness Program semantics Relations Unfold

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：