ICFP

As a company, Galois began its life with the mission simply of supplying functional programming services, building tools and products for clients, leveraging the productivity of functional languages and the abilities of our engineers. This went well, ...

Higher-order languages that encourage currying are implemented using one of two basic evaluation models: push/enter or eval/apply. Implementors use their intuition and qualitative judgements to choose one model or the other.Our goal in this paper is to ...

Programs in embedded languages contain invariants that are not automatically detected or enforced by their host language. We show how to use macros to easily implement partial evaluation of embedded interpreters in order to capture invariants encoded in ...

This paper presents an approach to searching for deadlocks in Concurrent Haskell programs. The search is based on a redefinition of the IO monad which allows the reversal of Concurrent Haskells concurrency primitives. Hence, it is possible to implement ...

There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more ...

Past attempts to relate two well-known models of backtracking computation have met with only limited success. We relate these two models using logical relations. We accommodate higher-order values and infinite computations. We also provide an ...

Sometimes it's worth doing things badly in order to do them fast. When is this the right plan? Are some kinds of mistakes worse than others? Could the right infrastructure make trial and error programming more effective? How will it play out in the ...

We extend Haskell with regular expression patterns. Regular expression patterns provide means for matching and extracting data which goes well beyond ordinary pattern matching as found in Haskell. It has proven useful for string manipulation and for ...

It is possible to extend the basic notion of "function call" to allow functions to have multiple return points. This turns out to be a surprisingly useful mechanism. This paper conducts a fairly wide-ranging tour of such a feature: a formal semantics ...

Recent functional logic languages such as Curry and Toy combine lazy functional programming with logic programming features including logic variables, non-determinism, unification, narrowing, fair search, concurrency, and residuation. In this paper, we ...

Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, so proving their soundness is ...

Abadi et al. introduced the dependency core calculus (DCC) as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a nonstandard ...

If a subexpression in a query will never contribute data to the query answer, this should be regarded as an error. This principle has been recently accepted into mainstream XML query languages, but was still waiting for a complete treatment. We provide ...

Useful type inference must be faster than normalization. Otherwise, you could check safety conditions by running the program. We analyze the relationship between bounds on normalization and type inference. We show how the success of type inference is ...

We study a type system equipped with universal types and equire-cursive types, which we refer to as F_͘. We show that type equality may be decided in time O(nlog n), an improvement over the previous known bound of O(n² ). In fact, we show that two more ...

It is now 20 years since the Ericsson Computer Science Laboratory (CSLab) was formed, and 20 years since CSLab started performing the programming language experiments that eventually led to the development of the Erlang programming language. For 15 ...

We present a process logic for the p -calculus with the linear/affine type discipline [6, 7, 31, 32, 33, 59, 60]. Built on the preceding studies on logics for programs and processes, simple systems of assertions are developed, capturing the classes of ...

Concurrency, as a useful feature of many modern programming languages and systems, is generally hard to reason about. Although existing work has explored the verification of concurrent programs using high-level languages and calculi, the verification of ...

Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. If we postulate soundness (in the sense that ...

Compilers structured as a small number of monolithic passes are difficult to understand and difficult to maintain. Adding new optimizations often requires major restructuring of existing passes that cannot be understood in isolation. The steep learning ...

This paper presents a methodology for implementing natural language morphology in the functional language Haskell. The main idea behind is simple: instead of working with untyped regular expressions, which is the state of the art of morphology in ...

Among slide-presentation systems, the dominant application offers essentially no abstraction capability. Slideshow, an extension of PLT Scheme, represents our effort over the last several years to build an abstraction-friendly slide system. We show how ...

A generic function is a function that can be instantiated on many data types to obtain data type specific functionality. Examples of generic functions are the functions that can be derived in Haskell, such as show, read, and '=='. The recent years have ...

Writing boilerplate code is a royal pain. Generic programming promises to alleviate this pain by allowing the programmer to write a generic "recipe" for boilerplate code, and use that recipe in many places. In earlier work we introduced the "Scrap your ...