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

Productive Coprogramming with Guarded Recursion

acm sigplan NOTICES 2013年第9期48卷 197-208页

作者： Atkey, Robert McBride, Conor Univ Strathclyde Glasgow G1 1XQ Lanark Scotland

Total functional programming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to terminate, e. g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a program generates an infinite amount of data, each piece will be generated in finite time. the theoretical underpinning for productive programming with infinite output is provided by the category theoretic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well-founded data like finite lists and trees. Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compositional, and severely complicate coprogramming. Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to coprogramming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano's guarded recursion. Clock variables allow us to "close over" the generation of infinite codata, and to make finite observations, something that is not possible with guarded recursion alone.

关键词： Languages theory Types Recursion coalgebras corecursion guarded recursion total functional programming

来源：评论

学校读者我要写书评

暂无评论

Higher-Order functional Reactive programming without Spacetime Leaks 13

Higher-Order Functional Reactive Programming without Spaceti...

引用

18th acm sigplan international conference on functional programming

作者： Krishnaswami, Neelakantan R. Max Planck Inst Software Syst MPI SWS Saarbrucken Germany

ISBN: (纸本)9781450323260

functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style. In this paper, we give a new language for higher-order reactive programming. Our language generalizes and simplifies prior type systems for reactive programming, by supporting the use of streams of streams, first-class functions, and higher-order operations. We also support many temporal operations beyond streams, such as terminatable streams, events, and even resumptions with first-class schedulers. Furthermore, our language supports an efficient implementation strategy permitting us to eagerly deallocate old values and statically rule out spacetime leaks, a notorious source of inefficiency in reactive programs. Furthermore, these memory guarantees are achieved without the use of a complex substructural type discipline. We also show that our implementation strategy of eager deallocation is safe, by showing the soundness of our type system with a novel step-indexed Kripke logical relation.

关键词： functional reactive programming Kripke logical relations temporal logic guarded recursion dataflow capabilities comonads

来源：评论

学校读者我要写书评

暂无评论

Experience Report: functional programming of mHealth Applications 13

Experience Report: Functional Programming of mHealth Applica...

引用

18th acm sigplan international conference on functional programming

作者： Petersen, Christian L. Goerges, Matthias Dunsmuir, Dustin Ansermino, J. Mark Dumont, Guy A. Univ British Columbia Vancouver BC V5Z 1M9 Canada

ISBN: (纸本)9781450323260

A modular framework for the development of medical applications that promotes deterministic, robust and correct code is presented. the system is based on the portable Gambit Scheme programming language and provides a flexible cross-platform environment for developing graphical applications on mobile devices as well as medical instrumentation interfaces running on embedded platforms. Real world applications of this framework for mobile diagnostics, telemonitoring and automated drug infusions are reported. the source code for the core framework is open source and available at: https://***/part-cw/lambdanative.

关键词： functional programming Scheme application programming medical systems cross-platform development

来源：评论

学校读者我要写书评

暂无评论

Interactive programming with Dependent Types

Interactive Programming with Dependent Types

引用

18th acm sigplan international conference on functional programming

作者： Norell, Ulf Univ Gothenburg Gothenburg Sweden

ISBN: (纸本)9781450323260

In dependently typed languages run-time values can appear in types, making it possible to give programs more precise types than in languages without dependent types. this can range from keeping track of simple invariants like the length of a list, to full functional correctness. In addition to having some correctness guarantees on the final program, assigning more precise types to programs means that you can get more assistance from the type checker while writing them. this is what I focus on here, demonstrating how the programming environment of AGDA can help you when developing dependently typed programs.

关键词： Design Languages theory Dependent types

来源：评论

学校读者我要写书评

暂无评论

programming and Reasoning with Algebraic Effects and Dependent Types 13

Programming and Reasoning with Algebraic Effects and Depende...

引用

18th acm sigplan international conference on functional programming

作者： Brady, Edwin Univ St Andrews Sch Comp Sci St Andrews Fife Scotland

ISBN: (纸本)9781450323260

One often cited benefit of pure functional programming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions with the outside world. Haskell solves this problem using monads to capture details of possibly side-effecting computations - it provides monads for capturing state, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects. Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.

关键词： Languages Verification Dependent Types Algebraic Effects

来源：评论

学校读者我要写书评

暂无评论

Mtac: A Monad for Typed Tactic programming in Coq 13

Mtac: A Monad for Typed Tactic Programming in Coq

引用

18th acm sigplan international conference on functional programming

作者： Ziliani, Beta Dreyer, Derek Krishnaswami, Neelakantan R. Nanevski, Aleksandar Vafeiadis, Viktor MPI-SWS Saarbruecken Germany IMDEA Software Institute Madrid Spain MPI-SWS Kaiserslautern Germany

ISBN: (纸本)9781450323260

Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers. We present Mtac, a lightweight but powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.

关键词： Interactive theorem proving custom proof automation Coq monads typed meta-programming tactics

来源：评论

学校读者我要写书评

暂无评论

Multi-polymorphic programming in bondi

Multi-polymorphic programming in bondi

引用

2013 9th acm sigplan Workshop on Generic programming, WGP 2013 - Co-located with the 18th acm sigplan international conference on functional programming, ICFP 2013

作者： Given-Wilson, thomas Huang, Freeman Jay, Barry NICTA Australia University of Technology Sydney Australia

ISBN: (纸本)9781450323895

the bondi programming language is multi-polymorphic, in that it supports four polymorphic programming styles within a small core of computation, namely a typed pattern calculus. bondi's expressive power is illustrated by considering the problem of assigning reviewers to a paper. As the context generalises from a committee to a committee with additional reviewers, to a conference, to a federation or confederation, the solution incorporates polymorphism familiar from the functional, generic functional, relational, path-based, and object-oriented programming styles, respectively. these experiments show that multi-polymorphic programming is both practical and desirable. Copyright © 2013 acm.

关键词： Pattern matching

来源：评论

学校读者我要写书评

暂无评论

Productive Coprogramming with Guarded Recursion 13

Productive Coprogramming with Guarded Recursion

引用

18th acm sigplan international conference on functional programming

作者： Atkey, Robert McBride, Conor Univ Strathclyde Glasgow G1 1XQ Lanark Scotland

ISBN: (纸本)9781450323260

关键词： Languages theory Types Recursion coalgebras corecursion guarded recursion total functional programming

来源：评论

学校读者我要写书评

暂无评论

the Bedrock Structured programming System Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier 13

The Bedrock Structured Programming System Combining Generati...

引用

18th acm sigplan international conference on functional programming

作者： Chlipala, Adam MIT CSAIL Cambridge MA USA

ISBN: (纸本)9781450323260

We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. the abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language;but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack.

关键词： generative metaprogramming interactive proof assistants low-level programming languages functional programming

来源：评论

学校读者我要写书评

暂无评论

functional Reactive programming with Liveness Guarantees As relations are to set-valued functions, so event sources are to behaviours

Functional Reactive Programming with Liveness Guarantees As ...

引用

18th acm sigplan international conference on functional programming

作者： Jeffrey, Alan Alcatel Lucent Bell Labs Murray Hill NJ USA

ISBN: (纸本)9781450323260

functional Reactive programming (FRP) is an approach to the development of reactive systems which provides a pure functional interface, but which may be implemented as an abstraction of an imperative event-driven layer. FRP systems typically provide a model of behaviours (total time-indexed values, implemented as pull systems) and event sources (partial time-indexed values, implemented as push systems). In this paper, we investigate a type system for event-driven FRP programs which provide liveness guarantees, that is every input event is guaranteed to generate an output event. We show that FRP can be implemented on top of a model of sets and relations, and that the isomorphism between event sources and behaviours corresponds to the isomorphism between relations and set-valued functions. We then implement sets and relations using a model of continuations using the usual double-negation CPS transform. the implementation of behaviours as pull systems based on futures, and of event sources as push systems based on the observer pattern, thus arises from first principles. We also discuss a Java implementation of the FRP model.

关键词： Design theory functional Reactive programming Concurrency Liveness

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：