We discuss the features of functional programming related to formal methods and an emerging paradigm, Cloud Computing. Formal methods are useful in developing highly reliable mission-critical software. However, in lig...
详细信息
ISBN:
(纸本)9789896740092
We discuss the features of functional programming related to formal methods and an emerging paradigm, Cloud Computing. Formal methods are useful in developing highly reliable mission-critical software. However, in light-weight formal methods, we do not rely on very rigorous means, such as theorem proofs. Instead, we use adequately less rigorous means, such as evaluation of pre/post conditions and testing specifications, to increase confidence in our specifications. Millions of tests may be conducted in developing highly reliable mission-critical software in a light-weight formal approach. We consider an approach to leveraging lightweight formal methods by using "Cloud." Given a formal specification language which has the features of functional programming, such as referential transparency, we can expect advantages of parallel processing. One of the basic foundations of VDM specification languages is Set Theory. The pre/post conditions and proof-obligations may be expressed in terms of set expressions. We can evaluate this kind of expression in a data-parallel style by using MapReduce framework for a huge set of test cases over cloud computing environments. Thus, we expect we can greatly reduce the cost of testing specifications in light-weight formal methods.
functional programming (FP) lets users focus on the business logic of their applications by providing them with high-level and composable abstractions. However, both automatic memory management schemes traditionally u...
详细信息
ISBN:
(纸本)9789819722990;9789819723003
functional programming (FP) lets users focus on the business logic of their applications by providing them with high-level and composable abstractions. However, both automatic memory management schemes traditionally used for FP, namely tracing garbage collection and reference counting, may introduce latencies in places that can be hard to predict, which limits the applicability of the FP paradigm. We reevaluate the use of lazy reference counting in single-threaded functional programming with guaranteed constant-time memory management, meaning that allocation and deallocation take only a bounded and predictable amount of time. This approach does not leak memory as long as we use uniform allocation sizes. Uniform allocation sizes were previously considered impractical in the context of imperative programming, but we find it to be surprisingly suitable for FP. Preliminary benchmark results suggest that our approach is practical, as its performance is on par with Koka's existing state-of-the-art implementation of reference counting for FP, sometimes even outperforming it. We also evaluate the effect of different allocation sizes on application performance and suggest ways of allowing large allocation in non-mission-critical parts of the program via Koka's effect system. We believe this potentially opens the door to many new industrial applications of FP, such as its use in real-time embedded software. In fact, the development of a high-level domain-specific language for describing latency-critical quantum physics experiments was one of the original use cases that prompted us to initiate this work.
The construction of reliable concurrent and distributed systems is an extremely difficult endeavour. For complex systems, it requires modular development strategies based on precise interface specifications that allow...
详细信息
ISBN:
(纸本)9781605585680
The construction of reliable concurrent and distributed systems is an extremely difficult endeavour. For complex systems, it requires modular development strategies based on precise interface specifications that allow the various modules to interact properly. In this extended abstract we are concerned with message passing systems where partners engage in long and complex interactions, as opposed to, say, remote procedure calls composed of a pair of simple interactions. Session types allow for the description of continuous series of interactions between several partners. In the simpler case, they detail protocols between two partners [Honda et al. 1998];recently the original setting was widened to encompass multiple partners [Honda et al. 2008]. In this paper we deal with binary sessions only. Through a running example we visit session types and a functional concurrent language equipped with buffered semantics. Apart from the traditional "well typed programs do not go wrong", the semantics proposed allows for two extra interesting results: the ability to predict the required buffer size, and that of anticipating an output with respect to an input operation.
Based on the state of our ongoing research into Language-Driven Software Development (LDSD) and Language-Oriented programming (LOP) we argue that the yet relatively unknown paradigm of concatenative programming is val...
详细信息
ISBN:
(纸本)9789896740092
Based on the state of our ongoing research into Language-Driven Software Development (LDSD) and Language-Oriented programming (LOP) we argue that the yet relatively unknown paradigm of concatenative programming is valuable for fundamental software engineering research and might prove to be a suitable foundation for future programming. To be sound, we formally introduce Concat, our research prototype of a purely functional concatenative language. The simplicity of Concat is contrasted by its expressiveness and a richness of inspiring approaches. Concatenative languages contribute a fresh and different sight on functional programming, which might help tackle challenges in LDSD/LOP from a new viewpoint.
FPGAs as commodities offer a resource for high-performance computation that is unmatched in flexibility and price/performance. As a lab, we are interested in high-level descriptions of computation and data, and how th...
详细信息
ISBN:
(纸本)9780769543017
FPGAs as commodities offer a resource for high-performance computation that is unmatched in flexibility and price/performance. As a lab, we are interested in high-level descriptions of computation and data, and how they may be customized to map effectively on FPGA fabrics. This paper describes our tool-chain, approach and methodology to FPGA utilization. We give a case study of the generation of a low density parity checking forward error correction algorithm, and discuss the specific challenges we faced with using FPGAs as our target.
Networks of communicating processes can be viewed as networks of stream transformers and programmed in a lazy functional language. Thus the correctness of concurrent systems can be reduced to the correctness of functi...
详细信息
Around thirty years ago, P. Martin-Löf [12] suggested that the intuitionistic theory of types, originally designed as a formal system for constructive mathematics, could be viewed as a programming language. The c...
详细信息
Traditional CPU design shows signs of fatigue, expressed as overwhelming security vulnerabilities. As we investigate functional programming as an alternative to the insecure, traditional imperative programming model, ...
详细信息
ISBN:
(纸本)9781728133201
Traditional CPU design shows signs of fatigue, expressed as overwhelming security vulnerabilities. As we investigate functional programming as an alternative to the insecure, traditional imperative programming model, the inexistence of a stable functional programming system infrastructure and code base acts as the classic chicken-and-egg problem. There is no functional programming basic software because there are no functional programming machines, and vice-versa. In this paper we attempt to break this cycle by designing a baseline platform that enables the research on the practical security properties of architectures under a discipline of full-stack functional programming.
Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augm...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augmented in order to also deal with symbolic values. In this paper, in contrast, we present an alternative approach that is based on a program instrumentation. Basically, the execution of the instrumented program in a standard environment produces a sequence of events that can be used to reconstruct the associated symbolic execution.
We develop a simple functional programming language aimed at manipulating infinite, but first-order definable structures, such as the countably infinite clique graph or the set of all intervals with rational endpoints...
详细信息
We develop a simple functional programming language aimed at manipulating infinite, but first-order definable structures, such as the countably infinite clique graph or the set of all intervals with rational endpoints. Internally, such sets are represented by logical formulas that define them, and an external satisfiability modulo theories (SMT) solver is regularly run by the interpreter to check their basic properties. The language is implemented as a Haskell module.
暂无评论