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

4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe)

作者： O'Connor, Liam UNSW Australia Sydney NSW Australia

ISBN: (纸本)9781450368155

A commonly-used technique in dependently-typed programming is to encode invariants about a data structure into its type, thus ensuring that the data structure is correct by construction. Unfortunately, this often necessitates the embedding of explicit proof terms within the data structure, which are not part of the structure conceptually, but merely supplied to ensure that the data invariants are maintained. As the complexity of the specifications in the types increases, these additional terms tend to clutter definitions, reducing readability. We introduce a technique where these proof terms can be supplied later, by constructing the data structure within a proof delay applicative functor. We apply this technique to Trip, our new language for Hoare-logic verification of imperative programs embedded in Agda, where our applicative functor is used as the basis for a verification condition generator, turning the typed holes of Agda into a method for stepwise derivation of a program from its specification in the form of a Hoare triple.

关键词： hoare logic agda verification conditions applicative functor types imperative programming

来源：评论

学校读者我要写书评

暂无评论

Finitism, imperative Programs and Primitive Recursion

Finitism, Imperative Programs and Primitive Recursion

引用

International Symposium on Logical Foundations of Computer Science (LFCS)

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

ISBN: (纸本)9783030367558;9783030367541

The finitistic philosophy of mathematics, critical of referencing infinite totalities, has been associated from its inception with primitive recursion. That kinship was not initially substantiated, but is widely assumed, and is supported by Parson's Theorem, which may be construed as equating finitistic reasoning with finitistic computing. In support of identifying PR with finitism we build on the generic framework of [7] and articulate a finitistic theory of finite partialstructures, and a generic imperative programming language for modifying them, equally rooted in finitism. The theory is an abstract generalization of Primitive Recursive Arithmetic, and the programming language is a generic generalization of first-order recurrence (primitive recursion). We then prove an abstract form of Parson's Theorem that links the two.

关键词： Finitism Primitive recursive arithmetic Finite partial functions Primitive recursive functions imperative programming Loop variant Parson's theorem

来源：评论

学校读者我要写书评

暂无评论

Knowledge-Based Explorable Extended Reality Environments 1st ed. 2020

Knowledge-Based Explorable Extended Reality Environments

引用

2020年

作者： Jakub Flotyński

来源：评论

学校读者我要写书评

暂无评论

Using Generic and Generated Components to Create Static Software Analysis Tools Faster

Using Generic and Generated Components to Create Static Soft...

引用

13th Pacific Rim Knowledge Acquisition Workshop (PKAW)

作者： Tippetts, Edward Univ Canberra Canberra ACT 2601 Australia

ISBN: (纸本)9783319133324;9783319133317

In today's software engineering tool landscape, many sophisticated imperative static source code analysis tools exist. However the implementations of these analyses are normally tied to specific languages, so must be recreated for any new or lesser-known languages. It can be burdensome for small groups of language developers or third party tool authors to devote the necessary resources to creating an analysis tool suite specifically for their language, so a number of less popular languages lack such automated tool support to the detriment of their users. As a solution this paper argues that multiple analysis algorithms exist which are applicable to almost any high-level imperative programming language, and that support for them can be added to a language cheaply with a high degree of automation. Pursuit of these would provide a new way of gathering knowledge about application structure for languages that have not previously enjoyed strong tool support.

关键词： Software Engineering Code analysis Code generation Fact extraction imperative programming

来源：评论

学校读者我要写书评

暂无评论

The Math Gap in an Inclusive CS1 Course 18

The Math Gap in an Inclusive CS1 Course

引用

49th ACM SIGCSE Technical Symposium on Computer Science Education (SIGCSE)

作者： Jordan, Kris Stein, Gabi Univ N Carolina Chapel Hill NC 27515 USA

ISBN: (纸本)9781450351034

This poster investigated the data from the past year of CS1 and found overwhelming evidence that students who have taken calculus are significantly more likely to succeed and less likely to fail that those who do not. On a Fall 2016 CS1 final exam, students who had not earned credit for a first course in college-level calculus were 2.8 times more likely to fail it than those who had (p=<0.0001,N=844). The mean final score for students with calculus was an 84, and those without was 61 (p=<0.0001). The result surprised the instructor, course staff, and faculty familiar with the course because the course itself does not emphasize mathematical or scientific computing. The course was Java-based, objects-early, and introduces both object-oriented and imperative programming fundamentals. The effect was evident across a range of problems, none seemingly requiring beyond basic algebra. In the Spring of 2017, the instructor and course staff set forth to explore these questions and close the math gap discovered in the Fall of 2016. This poster further proposes to develop interventions to aid those with a lower math maturity level through introducing a specialized CS1 to better accommodate those with a lower math maturity level by reducing the pace and installing prerequisites for the established CS1. Prospective Computer Science students at liberal arts colleges and universities enter with a wide range of mathematical backgrounds. Failing to acknowledge these disparities is demoralizing to students during their first course in CS and is counter-productive to inclusivity.

关键词： Math background Math programming CS1 Object-oriented programming imperative programming CS Education Inclusivity

来源：评论

学校读者我要写书评

暂无评论

imperative self-adjusting computation

引用

ACM SIGPLAN NOTICES 2008年第1期43卷 309-322页

作者： Acar, Umut A. Ahmed, Amal Blume, Matthias Toyota Technol Inst Chicago IL USA

Self-adjusting computation enables writing programs that can automatically and efficiently respond to changes to their data (e. g., inputs). The idea behind the approach is to store all data that can change over time in modifiable references and to let computations construct traces that can drive change propagation. After changes have occurred, change propagation updates the result of the computation by re-evaluating only those expressions that depend on the changed data. Previous approaches to self-adjusting computation require that modifiable references be written at most once during execution-this makes the model applicable only in a purely functional setting. In this paper, we present techniques for imperative self-adjusting computation where modifiable references can be written multiple times. We define a language SAIL (Self-Adjusting imperative Language) and prove consistency, i.e., that change propagation and from-scratch execution are observationally equivalent. Since SAIL programs are imperative, they can create cyclic data structures. To prove equivalence in the presence of cycles in the store, we formulate and use an untyped, step-indexed logical relation, where step indices are used to ensure well-foundedness. We show that SAIL accepts an asymptotically efficient implementation by presenting algorithms and data structures for its implementation. When the number of operations (reads and writes) per modifiable is bounded by a constant, we show that change propagation becomes as efficient as in the non-imperative case. The general case incurs a slowdown that is logarithmic in the maximum number of such operations. We describe a prototype implementation of SAIL as a Standard ML library.

关键词： languages design semantics algorithms self-adjusting computation incremental computation step-indexed logical relations imperative programming change propagation memoization mutable state

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

SEMANTICS, SPECIFICATION LOGIC, AND HOARE LOGIC OF EXACT REAL COMPUTATION

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2024年第2期20卷

作者： Park, Sewon Brausse, Franz Collins, Pieter Kim, Sunyoung Konecny, Michal Lee, Gyesik Mueller, Norbert Neumann, Eike Preining, Norbert Ziegler, Martin Korea Adv Inst Sci & Technol Sch Comp Daejeon South Korea Univ Manchester Manchester England Maastricht Univ Maastricht Netherlands Yonsei Univ Seoul South Korea Aston Univ Birmingham England Hankyong Natl Univ Anseong South Korea Univ Trier Trier Germany Swansea Univ Swansea Wales Cornell Tech arXiv Komatsu Japan

We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language -theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits;expansions support additional primitive operations (such as a user -defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the 'precision' embedding Z is not an element of p 7 -> 2p is an element of R, we arrive at a first -order theory which we prove to be decidable and model -complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.

关键词： Computable Analysis Reliable Numerics imperative programming Turing- Completeness Decidability Hoare Logic Kleene Logic

来源：评论

学校读者我要写书评

暂无评论

Capsules and Closures

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2011年 276卷 191-213页

作者： Jeannin, Jean-Baptiste Cornell Univ Dept Comp Sci Ithaca NY 14853 USA

Capsules are a clean representation of the state of a computation in higher-order programming languages with effects. Their intent is to simplify and replace the notion of closure. They naturally provide support for functional and imperative features, including recursion and mutable bindings, and ensure lexical scoping without the use of closures, heaps, stacks or combinators. We present a comparison of the use of closures and capsules in the semantics of higher-order programming languages with effects. In proving soundness of one to the other, we give a precise account of how capsule environments and closure environments relate to each other.

关键词： Capsule Closure Functional programming imperative programming State of Computation Higher-Order Functions Mutable Variables Scoping programming Language Semantics

来源：评论

学校读者我要写书评

暂无评论

Reasoning about efficiency within a probabilistic μ-calculus

引用

Electronic Notes in Theoretical Computer Science 1999年 22卷 138-155页

作者： A.K. McIver Programming Research Group Oxford University UK

Expectation-based probabilistic predicate transformers [15] provide a logic for probabilistic sequential programs, giving access to expressions such as ‘the probability that predicate A is achieved finally’. Using expectations more generally however, we can express μ-calculus formulae for the expected path-length of a computation tree. Moreover within an expectation-based μ-calculus such efficiency measures and more conventional (but probabilistic) temporal operators [14] can be related.

关键词： Probabilistic semantics predicate transformers nondeterminism verification refinement imperative programming time efficiency, complexity

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：