7,482 papers · page 224 of 375
Write it recursively: a generic framework for optimal path queries
Experience report: a pure shirt fits
Bluespec is a hardware-design tools startup whose core technology is developed using Haskell. Haskell is an unusual choice for a startup because it adds technical risk to the inherent business risk. In the years since Bluespec's founding, we have discovered that Haskell's purity …
Ynot: dependent types for imperative programs
We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language i…
The power of Pi
This paper exhibits the power of programming with dependent types by dint of embedding three domain-specific languages: Cryptol, a language for cryptographic protocols; a small data description language; and relational algebra. Each example demonstrates particular design patterns…
Functional netlists
In efforts to overcome the complexity of the syntax and the lack of formal semantics of conventional hardware description languages, a number of functional hardware description languages have been developed. Like conventional hardware description languages, however, functional ha…
From ML to MLF: graphic type constraints with efficient type inference
MLF is a type system that seamlessly merges ML-style type inference with System-F polymorphism. We propose a system of graphic (type) constraints that can be used to perform type inference in both ML or MLF. We show that this constraint system is a small extension of the formalis…
Type checking with open type functions
We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entail…
Space profiling for parallel functional programs
This paper presents a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to program source code. Unlike many profiling tools, our profiler is based on a cost s…
FPH: first-class polymorphism for Haskell
Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting "firstclass" polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a …
QVM: an efficient runtime for detecting defects in deployed systems
Coping with software defects that occur in the post-deployment stage is a challenging problem: bugs may occur only when the system uses a specific configuration and only under certain usage scenarios. Nevertheless, halting production systems until the bug is tracked and fixed is …
A theory of aspects as latent topics
After more than 10 years, Aspect-Oriented Programming (AOP) is still a controversial idea. While the concept of aspects appeals to everyone's intuitions, concrete AOP solutions often fail to convince researchers and practitioners alike. This discrepancy results in part from a lac…
Verifying correct usage of atomic blocks and typestate
The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software. However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level …
Efficient local type inference
Inference of static types for local variables in Java bytecode is the first step of any serious tool that manipulates bytecode, be it for decompilation, transformation or analysis. It is important, therefore, to perform that step as accurately and efficiently as possible. Previou…
Tolerating memory leaks
Type safety and garbage collection in managed languages eliminate memory errors such as dangling pointers, double frees, and leaks of unreachable objects. Unfortunately, a program still leaks memory if it maintains references to objects it will never use again. Leaked objects dec…
A tag-based approach for the design and composition of information processing applications
In the realm of component-based software systems, pursuers of the holy grail of automated application composition face many significant challenges. In this paper we argue that, while the general problem of automated composition in response to high-level goal statements is indeed …
The impact of static-dynamic coupling on remodularization
We explore the concept of static-dynamic coupling--the degree to which changes in a program's static modular structure imply changes to its dynamic structure. This paper investigates the impact of static-dynamic coupling in a programming language on the effort required to evolve …
Enabling static analysis for partial java programs
Software engineering tools often deal with the source code of programs retrieved from the web or source code repositories. Typically, these tools only have access to a subset of a program's source code (one file or a subset of files) which makes it difficult to build a complete a…
jStar: towards practical verification for java
In this paper we introduce a novel methodology for verifying a large set of Java programs which builds on recent theoretical developments in program verification: it combines the idea of abstract predicate families and the idea of symbolic execution and abstraction using separati…
Safer unsafe code for .NET
The.NET intermediate language (MSIL) allows expressing both statically verifiable memory and type safe code (typi-cally called managed), as well as unsafe code using direct pointer manipulations. Unsafe code can be expressed in C# by marking regions of code as unsafe. Writing uns…