916 papers · page 40 of 46
Abstract Compiler generation based on Mosses' action semantics has been studied by Brown, Moura, and Watt, and also by the second author. The core of each of their systems is a handwritten action compiler, producing either C or machine code. We have obtained an action compiler in…
Abstract Brodal recently introduced the first implementation of imperative priority queues to support findMin, insert and meld in O (1) worst-case time, and deleteMin in O (log n ) worst-case time. These bounds are asymptotically optimal among all comparison-based priority queues…
Abstract A substantial amount of work has been devoted to the proof of correctness of various program analyses but much less attention has been paid to the correctness of compiler optimisations based on these analyses. In this paper we tackle the problem in the context of strictn…
Abstract The paper explores the application of a lazy functional language, Haskell, to a series of grid-based scientific problems—solution of the Poisson equation, and Monte Carlo simulation of two theoretical models from statistical and particle physics. The implementations intr…
Abstract We develop an operational model for a language based on linear logic. Our semantics is ‘low-level’ enough to express sharing and copying while still being ‘high-level’ enough to abstract away from details of memory layout, and thus can be used to test potential applicati…
Abstract This paper makes a contribution to the refinement of systems which involve search by proposing a simple non-deterministic model for rule based transition systems and using this to define a meaning for rule based refinement which allows each stage of the software developm…
Abstract We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic extensions of it. The λ-calculus extended with surjective pairing has been well-studied i…
Abstract This paper describes a compiling graph reduction system which realizes the reduction semantics of a fully-fledged applied λ-calculus. High-level functional programs are conceptually executed as sequences of program transformations governed by full β-reductions. They may …
Abstract The tree-drawing problem is to produce a ‘tidy’ mapping from elements of a tree to points in the plane. In this paper, we derive an efficient algorithm for producing tidy drawings of trees. The specification, the starting point for the derivations, consists of a collecti…
Abstract The Third Homomorphism Theorem is a folk theorem of the constructive algorithmics community. It states that a function on lists that can be computed both from left to right and from right to left is necessarily a list homomorphism – it can be computed according to any pa…
Abstract This paper investigates several sparse matrix representation schemes and associated algorithms in Haskell for solving linear systems of equations arising from solving realistic computational fluid dynamics problems using a finite element algorithm. This work complements …
Abstract The weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the i…
Abstract We study the operational semantics of an extension of Girard's System F ω with two control operators: an abort operation that abandons the current control context, and a callcc operation that captures the current control context. Two classes of operational semantics are …
Abstract Over 25 implementations of different functional languages are benchmarked using the same program, a floating-point intensive application taken from molecular biology. The principal aspects studied are compile time and execution time for the various implementations that w…
Abstract The resource constrained shortest path problem is an NP-hard problem for which many ingenious algorithms have been developed. These algorithms are usually implemented in Fortran or another imperative programming language. We have implemented some of the simpler algorithm…
Abstract This paper describes a scheme for constructing parsers based on the top-down combinator approach. In particular, it describes a set of combinators for parsing expressions described by ambiguous grammars with precedence and associativity rules. The new combinators embody …
Abstract We have developed a simple algebraic approach to music description and composition called Haskore . In this framework, musical objects consist of primitive notions such as notes and rests, operations to transform musical objects such as transpose and tempo-scaling, and o…
Abstract A number of difficulties in the formalism of Pure Type Systems (PTS) is discussed and an alternative classification system for typed calculi is proposed. In the new approach the main novelty is that one first explicitly specifies the dependencies that may occur. This is …
Abstract In this article, we extend the Barendregt Cube with ∏-conversion (which is the analogue of β-conversion, on product type level) and study its properties. We use this extension to separate the problem of whether a term is typable from the problem of what is the type of a …