1,066 papers · page 38 of 54
C-Rules is a business rules management system developed by Constraint Technologies International1 (CTI), designed for use in transportation problems. Users define rules describing various aspects of a problem, such as solution costs and legality, which are then queried from a hos…
Over the past year Untyped has developed some 40'000 lines of Scheme code for a variety of web-based applications, which receive over 10'000 hits a day. This is, to our knowledge, the largest web-based application deployment of PLT Scheme. Our experiences developing with PLT Sche…
The Dependency Core Calculus (DCC) is an extension of the computational lambda calculus that was designed in order to capture the notion of dependency that arises in information-flow control, partial evaluation, and other programming-language settings. We show that, unexpectedly,…
In 1991, when the Journal of Functional Programming was inaugurated, the editors, Simon Peyton Jones and Philip Wadler, asked me to contribute a regular column to be called Functional Pearls. The idea was to emulate the very successful series of essays that Jon Bentley had writte…
We present language mechanisms for polymorphic, extensible records and their exact dual, polymorphic sums with extensible first-class cases. These features make it possible to easily extend existing code with new cases. In fact, such extensions do not require any changes to code …
This paper introduces a pattern for almost compositional functions over recursive data types, and over families of mutually recursive data types. Here "almost compositional" means that for a number of the constructors in the type(s), the result of the function depends only on the…
I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's…
In most programming languages, type abstraction is guaranteed by syntactic scoping in a single program, but is not preserved by marshalling during distributed communication. A solution is to generate hash types at compile time that consist of a fingerprint of the source code impl…
Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional events, which combines first-class synchronous messagepassing events with all-or…
The problem of expressing I/O and side effects in functional languages is a well-established one. This paper addresses this problem from a general semantic viewpoint by giving a unified framework for describing shared state, I/O and deterministic concurrency. We develop a modifie…
Chez Scheme is now over 20 years old, the first version having been released in 1985. This paper takes a brief look back on the history of Chez Scheme's development to explore how and why it became the system it is today.
We describe an s-expression based syntax-extension framework much like Scheme macros, with a key additional facility: the ability to define static semantics, such as type systems or program analysis, for the new, user-defined forms or embedded languages, thus allowing us to const…
This paper presents the core type system and type inference algorithm of OCamlDuce, a merger between OCaml and XDuce. The challenge was to combine two type checkers of very different natures while preserving the best properties of both (principality and automatic type reconstruct…
We investigate the development of a general-purpose framework for mechanized reasoning about the meta-theory of programming languages. In order to provide a standard, uniform account of a programming language, we propose to define it as a logic in a logical framework, using the s…
Generalized algebraic data types (GADTs), sometimes known as “guarded recursive data types ” or “first-class phantom types”, are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although…
We present a unifying solution to the problem of fusion of functions, where both the producer function and the consumer function have one accumulating parameter. The key idea in this development is to formulate the producer function as a function which computes over a monoid of d…
Often, independent organizations define and advocate different XML formats for a similar purpose and, as a result, application programs need to mutually convert between such formats. Existng XML transformation languages, such as XSLT and XDuce, are unsatisfactory for this purpose…
Dynamic binding and delimited control are useful together in many settings, including Web applications, database cursors, and mobile code. We examine this pair of language features to show that the semantics of their interaction is ill-defined yet not expressive enough for these …
Monads are widely used in Haskell for modeling computational effects, but defining monads remains a daunting challenge. Since every part of a monad's definition depends on its computational effects, programmers cannot leverage the common behavior of all monads easily and thus mus…
We present two independent and complementary improvements for flow-based analysis of higher-order languages: (1) abstract garbage collection and (2) abstract counting, collectively titled ΓCFA.Abstract garbage collection is an analog to its concrete counterpart: we determine when…