1,066 papers · page 39 of 54
TheML module system is useful for building large-scale programs. The programmer can factor programs into nested and parameterized modules, and can control abstraction with signatures. Yet ML prohibits recursion between modules. As a result of this constraint, the programmer may h…
In previous work, we proposed a Hoare Type Theory (HTT) which combines effectful higher-order functions, dependent types and Hoare Logic specifications into a unified framework. However, the framework did not support polymorphism, and ailed to provide a modular treatment of state…
Component programming techniques encourage abstraction and reuse through external linking. Some parts of a program, however, must use concrete, internally specified references, so a pure component system is not a sufficient mechanism for structuring programs. We present the combi…
Despite its powerful module system, ML has not yet evolved for the modern world of dynamic and open modular programming, to which more primitive languages have adapted better so far. We present the design and semantics of a simple yet expressive firstclass component system for ML…
This paper gives a precise characterization for the complexity of the problem of proving equal two streams defined with a finite number of equations: Π0 over 2. Since the Π 0 over 2 class includes properly both the reursively enumerable and the corecursively enumerable classes, t…
No abstract available.
Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the virtues of two well-established…
A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored values. While the likelihood that such t…
Transient faults that arise in large-scale software systems can often be repaired by re-executing the code in which they occur. Ascribing a meaningful semantics for safe re-execution in multi-threaded code is not obvious, however. For a thread to correctly rexecute a region of co…
The concept of a “unique” object arises in many emerging programming languages such as Clean, CQual, Cyclone, TAL, and Vault. In each of these systems, unique objects make it possible to perform operations that would otherwise be prohibited (e.g., deallocating an object) or to en…
We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data structures. The program logi…
Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, they express the programmer's intent somewhat indirectly. Developi…
1. Introduction The notion of type equality plays a pivotal r^ole in type systemdesign. However, the importance of this role is often less evident in commonly studied type systems. For instance, in the simplytyped
This paper defines PolyAML, a typed functional, aspect-oriented programming language. The main contribution of PolyAML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers …
This paper explains how the high-level treatment of datatypes in functional languages—using features like constructor functions and pattern matching—can be made to coexist with bitdata. We use this term to describe the bit- level representations of data that are required in the c…
Existential types provide a simple and elegant foundation for understanding generative abstract data types, of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found that the traditional existenti…
This talk presents the tumultuous history of JavaScript, from its first appearance in Netscape 2 beta releases in the fall of 1995 through the present, with emphasis on the unvarnished, real-world side of designing, implementing, shipping, and standardizing a functional programmi…
Proof-carrying code (PCC) is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems and typed assembly languages, however, can only handle sequential programs. This severely limits their applicability sinc…
Monads are commonplace programming devices that are used to uniformly structure computations with effects such as state, exceptions, and I/O. This paper further develops the monadic programming paradigm by investigating the extent to which monadic computations can be optimised by…