C-Rules is a business rules management system developed by Constraint Technologies International (www.constrainttechnologies.com) that is designed for use in transport, travel and logistics problems. Individual businesses within these industries often need to solve the same kinds of problems related to scheduling of operations, resource allocation, staff rostering and so on, but each organisation has its own rules and procedures. Furthermore, these problems tend to be combinatorially challenging: before a final solution is chosen, many potential choices need to be generated, evaluated and compared. In C-Rules, users define rules that describe various aspects of a problem. These rules can be invoked from an application, which is typically either an optimising solver or an interactive planning tool. Rules can be used to encode evaluation criteria, such as the legality or cost of a proposed solution, or values like configuration parameters that may be used by the host application to tune or direct its progress. At its core, C-Rules provides a functional expression language that affords users power and flexibility when formulating rules. In this paper we will describe our experiences of using functional programming both at the end-user level and at the implementation level. We highlight some of the benefits of basing our rule system on features such as higher-order functions, referential transparency and static, polymorphic typing. We also outline some of our experiences in using Haskell to build an efficient compiler for the core language.

Transient faults that arise in large-scale software systems can often be repaired by reexecuting the code in which they occur. Ascribing a meaningful semantics for safe reexecution in multithreaded code is not obvious, however. For a thread to reexecute correctly a region of code, it must ensure that all other threads that have witnessed its unwanted effects within that region are also reverted to a meaningful earlier state. If not done properly, data inconsistencies and other undesirable behavior might result. However, automatically determining what constitutes a consistent global checkpoint is not straightforward because thread interactions are a dynamic property of the program. In this paper, we present a safe and efficient checkpointing mechanism for Concurrent ML (CML) that can be used to recover from transient faults. We introduce a new linguistic abstraction, called stabilizers, that permits the specification of per-thread monitors and the restoration of globally consistent checkpoints. Safe global states are computed through lightweight monitoring of communication events among threads (e.g., message-passing operations or updates to shared variables). We present a formal characterization of its design, and provide a detailed description of its implementation within MLton, a whole-program optimizing compiler for Standard ML. Our experimental results on microbenchmarks as well as several realistic, multithreaded, server-style CML applications, including a web server and a windowing toolkit, show that the overheads to use stabilizers are small, and lead us to conclude that they are a viable mechanism for defining safe checkpoints in concurrent functional programs.

Propositions that express type equality are a frequent ingredient of modern functional programming – they can encode generic functions, dynamic types, and GADTs. Via the Curry–Howard correspondence, these propositions are ordinary types inhabited by proof terms, computed using runtime type representations. In this paper we show that two examples of type equality propositions actually do reflect type equality; they are only inhabited when their arguments are equal and their proofs are unique (up to equivalence.) We show this result in the context of a strongly normalizing language with higher-order polymorphism and primitive recursion over runtime-type representations by proving Reynolds's abstraction theorem. We then use this theorem to derive “free” theorems about equality types.