In this paper we investigate writing and using of a functional parallel-machine simulator, in a functional programming language as opposed to an imperative programminglanguage, in terms of code-size, versatility and ...
详细信息
ISBN:
(纸本)9781510642720
In this paper we investigate writing and using of a functional parallel-machine simulator, in a functional programming language as opposed to an imperative programminglanguage, in terms of code-size, versatility and performance. As a use-case we chose a SIMD-type machine, and the Racket/Scheme programminglanguage,. The main advantages over the use of imperative programminglanguages for creating architectural simulators are (i)divided by the loose coupling to the architecture and (ii) the lack of an explicit compiler. By attempting two common software implementations and some changes to the base architecture we argue that the simulator is better in terms of algorithm-code size and system versatility (number of required changes for extending functionality) but not in execution speed (as it is running on a von Neumann machine, where C++ code is compiled into native machine code, not interpreted)
In this paper, we study the mechanism for extracting the environment from a function closure in the framework of the lambda calculus. We propose the lambda calculus with environment extraction, which extends environme...
详细信息
We present a new modular proof method of termination for second-order computation, and report its implementation SOL. The proof method is useful for proving termination of higher-order foundational calculi. To establi...
详细信息
We present a new modular proof method of termination for second-order computation, and report its implementation SOL. The proof method is useful for proving termination of higher-order foundational calculi. To establish the method, we use a variation of the semantic labelling translation and Blanqui's General Schema: a syntactic criterion of strong normalisation. an application, we show termination of a variant of call-by-push-value calculus with algebraic effects, an effect handler and effect theory. We also show that our tool SOL is effective to solve higher-order termination problems.
The Curry-Howard isomorphism shows that an intuitionistic deductive system is similar to a formal computational system;propositions correspond to types, proofs to lambda-terms, and a proof normalization procedure to a...
详细信息
ISBN:
(纸本)9781450365734
The Curry-Howard isomorphism shows that an intuitionistic deductive system is similar to a formal computational system;propositions correspond to types, proofs to lambda-terms, and a proof normalization procedure to an evaluation strategy. Furthermore, the duality between computation values and continuations is discovered under the Curry-Howard isomorphism. In the traditional lambda calculus, duplication and erasing of values are allowed but those of continuations prohibited. On the other hand, in the lambda calculus with first-class continuations, both values and continuations are permitted to be duplicated and erased. In our previous paper, we proposed a linear lambda calculus with first-class continuations, in which we cannot duplicate and erase values but can do continuations. In this paper, we propose an ML polymorphic type system for the linear lambda calculus with first-class continuations and design a type inference algorithm of the type system.
作者：
Chlipala, AdamMIT
CSAIL 77 Massachusetts Ave Cambridge MA 02139 USA
The World Wide Web has evolved gradually from a document delivery platform to an architecture for distributed programming. This largely unplanned evolution is apparent in the set of interconnected languages and protoc...
详细信息
The World Wide Web has evolved gradually from a document delivery platform to an architecture for distributed programming. This largely unplanned evolution is apparent in the set of interconnected languages and protocols that any Web application must manage. This paper presents Ur/Web, a domain-specific, statically typed functional programming language with a much simpler model for programming modern Web applications. Ur/Web's model is unified, where programs in a single programminglanguage are compiled to other "Web standards" languages as needed;supports novel kinds of encapsulation of Web-specific state;and exposes simple concurrency, where programmers can reason about distributed, multithreaded applications via a mix of transactions and cooperative preemption. We give a tutorial introduction to the main features of Ur/Web.
The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and con...
详细信息
The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functionallanguages with respect to logical negation. My previous paper and other researchers' studies reveal that we can obtain a first-class continuation mechanism by providing duplicability and removability of continuations, which is equivalent to the rightcontraction and weakening rules in Gentzen's deductive system, the sequent calculus. In the lambda calculus, it is allowed to duplicate and remove values, but the continuations are impossible to duplicate and remove. In our previous paper, we showed that we can obtain the lambda calculus with first-class continuations providing duplicability and removability of both values and continuations. In this paper, we will study a calculus in which we only have duplicability and removability of continuations. We formalize this calculus in the framework of linear logic, which is a logical system sensitive to duplicability and removability, proposed by Jean-Yves Girard.
It is difficult to knowall the relations between Snort rules. To deal with this problem, the topological relations between Snort rules are classified based on the set theory, and a method for calculating the topologic...
详细信息
It is difficult to knowall the relations between Snort rules. To deal with this problem, the topological relations between Snort rules are classified based on the set theory, and a method for calculating the topological relations between Snort rules is proposed. In the existing methods for analyzing the relations of Snort rules, the relations are usually determined only according to the header information of the Snort rules. Without considering the actions of Snort rules, the proposed method improves upon the existing methods and it can classify and calculate the topological relations between Snort rules according to both headers and options information of Snort rules. In addition, the proposed method is implemented by the functionallanguage Haskell. The experimental results showthat the topological relations between Snort rules can be calculated rapidly and effectively. The proposed method also provides an important basis for conflict detection in the succeeding Snort rules.
Set of Software Quality Static Analyzers (SSQSA) is a framework which includes set of software tools for static analysis. Starting aim of the framework is consistent software quality analysis. The main characteristic ...
详细信息
ISBN:
(纸本)9780735412873
Set of Software Quality Static Analyzers (SSQSA) is a framework which includes set of software tools for static analysis. Starting aim of the framework is consistent software quality analysis. The main characteristic of all integrated tools is the independency of the input programminglanguage. Each of the integrated analysers can be uniformly applied to any software systems that are written in different programminglanguages. In SSQSA framework, language independency is achieved by enriched Concrete Syntax Tree (eCST). eCST is used as an internal representation of the source code. Currently, SSQSA supports some representative input languages. Still the support for functionallanguage is missing. For introducing the support for new input language into SSQSA framework straightforward semi-automated procedure is established. In this paper we explore possibility to add support for functionallanguages into SSQSA framework. Furthermore, we describe alternative way to add support for new language. Described research is made on the case of Erlang.
Interactive programs, like user interfaces, are hard to formally specify and thus to prove correct. Some ideas coming from functional programming languages have been successful to improve the way we write safer progra...
详细信息
ISBN:
(纸本)9781467370431
Interactive programs, like user interfaces, are hard to formally specify and thus to prove correct. Some ideas coming from functional programming languages have been successful to improve the way we write safer programs, compared to traditional imperative languages, but these ideas mostly apply to code fragments without any inputs-outputs. Using the purely functionallanguage Coq, we present a new technique to represent interactive programs and formally verify use cases using the Coq proof engine as a symbolic debugger. To this end we introduce the notion of scenarios, well-typed schema of interactions between an environment and a program. We design and certify a blog system as an illustration. Our approach generalizes unit-testing techniques and outlines a new method for mechanically assisted checking of effectful functional programs.
Pawns is a programminglanguage under development that supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features incl...
详细信息
Pawns is a programminglanguage under development that supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures that are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and post-conditions concerning sharing for functions.
暂无评论