We report on our experience using functionalprogramming languages in the development of a commercial GNU/Linux distribution, discussing features of several significant systems: hardware detection and system configura...
详细信息
functional Reactive programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such a...
详细信息
ISBN:
(纸本)9781450351829
functional Reactive programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such as having a fixed time domain, time always flowing forward, and limiting the exploration of the past. In this paper we show how these constraints can be overcome, giving local control over the time domain, the direction of time and the sampling step. We study the behaviour of FRP expressions when time flows backwards, and demonstrate how to synchronize subsystems running asynchronously and at different sampling rates. We have verified the practicality of our approach with two non-trivial games in which time control is central to the gameplay.
Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adopti...
详细信息
ISBN:
(纸本)9781450336871
Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programmingthem and the low-level control of the hardware required to achieve good performance. this paper suggests a programming library, SafeGPU, that aims at striking a balance between programmer productivity and performance, by making GPU data-parallel operations accessible from within a classical object-oriented programming language. the solution is integrated withthe design-by-contract approach, which increases confidence in functional program correctness by embedding executable program specifications into the program text. We show that our library leads to modular and maintainable code that is accessible to GPGPU non-experts, while providing performance that is comparable with hand-written CUDA code. Furthermore, runtime contract checking turns out to be feasible, as the contracts can be executed on the GPU.
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...
详细信息
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.
Representing a syntax tree using a data type often involves having many similar-looking constructors. Functions operating on such types often end up having many similar-looking cases. Different languages often make us...
详细信息
ISBN:
(纸本)9781450310543
Representing a syntax tree using a data type often involves having many similar-looking constructors. Functions operating on such types often end up having many similar-looking cases. Different languages often make use of similar-looking constructions. We propose a generic model of abstract syntax trees capable of representing a wide range of typed languages. Syntactic constructs can be composed in a modular fashion enabling reuse of abstract syntax and syntactic processing within and across languages. Building on previous methods of encoding extensible data types in Haskell, our model is a pragmatic solution to Wadler's "expression problem". Its practicality has been confirmed by its use in the implementation of the embedded language Feldspar.
the 17thacmsigplaninternationalconference on functionalprogramming (ICFP) took place on September 10–12, 2012 in Copenhagen, Denmark. After the conference, the programme committee selected several outstanding pa...
详细信息
the 17thacmsigplaninternationalconference on functionalprogramming (ICFP) took place on September 10–12, 2012 in Copenhagen, Denmark. After the conference, the programme committee selected several outstanding papers and invited their authors to submit to this special issue of Journal of functionalprogramming. Robby Findler and Satnam Singh acted as editors for these submissions. this issue includes the accepted papers, each of which provides substantial new material beyond the original conference version. [ABSTRACT FROM AUthOR]
De Bruijn indices are a well known technique for programming with names and binders. they provide a representation that is both simple and canonical. However, programming errors tend to be really easy to make. We prop...
详细信息
ISBN:
(纸本)9781450308656
De Bruijn indices are a well known technique for programming with names and binders. they provide a representation that is both simple and canonical. However, programming errors tend to be really easy to make. We propose a safer programming interface implemented as a library. Whereas indexing the types of names and terms by a numerical bound is a famous technique, we index them by worlds, a different notion of index that is both finer and more abstract. While being more finely typed, our approach incurs no loss of expressiveness or efficiency. Via parametricity we obtain properties about functions polymorphic on worlds. For instance, well-typed world-polymorphic functions over open lambda-terms commute with any renaming of the free variables. Our whole development is conducted within Agda, from the code of the library, to its soundness proof and the properties of external functions. the soundness of our library is demonstrated via the construction of a logical relations argument.
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 invaria...
详细信息
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.
Dynamic programming Languages, such as Java, JavaScr ipt, PHP, Perl, Python, Ruby, etc., are dominating languages for programmingthe web. HW/SW co-designed virtual machine can significantly accelerate their execution...
详细信息
ISBN:
(纸本)9781450320856
Dynamic programming Languages, such as Java, JavaScr ipt, PHP, Perl, Python, Ruby, etc., are dominating languages for programmingthe web. HW/SW co-designed virtual machine can significantly accelerate their executions by transparently leveraging internal HW features via an internal compiler. We also argue for a common API to interface dynamic languages withthe HW/SW co-designed virtual machine, so that a single internal compiler can accelerate all major dynamic languages.
暂无评论