1,066 papers · page 35 of 54
ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into mutually recursive, separately compilable components. Mixin modules facilitate recursive linking of s…
Transactional events (TE) are an approach to concurrent programming that enriches the first-class synchronous message-passing of Concurrent ML (CML) with a combinator that allows multiple messages to be passed as part of one all-or-nothing synchronization. Donnelly and Fluet (200…
The trend in microprocessor design toward multicore and manycore processors means that future performance gains in software will largely come from harnessing parallelism. To realize such gains, we need languages and implementations that can enable parallelism at many different le…
There are now a number of BIDIRECTIONAL PROGRAMMING LANGUAGES, where every program can be read both as a forward transformation mapping one data structure to another and as a reverse transformation mapping an edited output back to a correspondingly edited input. Besides parsimony…
There has been a lot of interest of late for programming languages that incorporate features from dependent type systems and proof assistants, in order to capture important invariants of the program in the types. This allows type-based program verification and is a promising comp…
We introduce the notion of discrimination as a generalization of both sorting and partitioning and show that worst-case linear-time discrimination functions (discriminators) can be defined generically, by (co-)induction on an expressive language of order denotations. The generic …
Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive data type, operations on streams are implemented by corecursive programs, and proofs are conducted using coinduction. But there is more to it: suitably restricted, stream equations possess…
We give an exact characterization of the computational complexity of the kCFA hierarchy. For any k> 0, we prove that the con-trol flow decision problem is complete for deterministic exponen-tial time. This theorem validates empirical observations that such control flow analysis i…
This paper presents AURA, a programming language for access control that treats ordinary programming constructs (e.g., integers and recursive functions) and authorization logic constructs (e.g., principals and access control policies) in a uniform way. AURA is based on polymorphi…
This paper describes our experience using a functional language, Haskell, to build an embedded, domain-specific language (DSL) for component configuration in large-scale, real-time, embedded systems. Prior to the introduction of the DSL, engineers would describe the steps needed …
With features that include lightweight syntax, expressive type systems, and deep semantic foundations, functional languages are now being used to develop an increasingly broad range of complex, real-world applications. In the area of systems software, however, where performance a…
In the context of program verification in an interactive theorem prover, we study the problem of transforming function definitions with ML-style (possibly overlapping) pattern matching into minimal sets of independent equations. Since independent equations are valid unconditional…
HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism. In contrast to other proposals, HML uses regular System F types and has a simple type inference algorithm that is just a small extension of the usual Damas-Milner algorithm W. Given th…
Self-adjusting programs respond automatically and efficiently to input changes by tracking the dynamic data dependences of the computation and incrementally updating the output as needed. In order to identify data dependences, previously proposed approaches require the user to ma…