Scottish Programming Languages Seminar

Jeremy Siek: Monads for Relations

Monads provide a framework for writing modular and concise specifications for functions that appear to have computational effects. For example, an interpreter for a language with references can be written in Haskell as a function over a state monad. But what if we wish to define a relation, not a function? Suppose we want to define a natural semantics for a language with references. Natural semantics are inductively defined relations, not functions, so monads are not directly applicable. But can we adapt monads to relations? The answer is yes; I show how in this talk. I follow a similar structure to Wadler's ``The essence of functional programming,'' defining several extensions to the lambda calculus, but via natural semantics instead of interpreters.

Greg Michaelson: Costing by Construction

Jon Lewis: Insense: a component-based language for self-configuring and self-healing wireless sensor network applications

Wireless sensor networks (WSNs) are complex, distributed systems whose components are commonly expected to operate in the face of unforeseen changes to the environment. WSN applications must be self-aware to be capable of adapting in response to such changes. We address this requirement with a high-level, component-based language model and implementation. In Insense, a sensing system is modelled as a composition of software components that interact via channels that may be published to the network and used to identify services available to other networked components. The language permits an application to dynamically discover both network topology and channels that have been published for inter-node use. Self-configuring application components are thereby able to search for the service channels they require and access these by configuring the channel bindings. Self-healing is supported by an exception model permitting components to detect channel communication anomalies and through language mechanisms permitting applications to be dynamically reconfigured.

Seyed H Haeri: Observational Equivalence between Lazy Programs in Presence of Selective Strictness.

Gabbay et al. were first to consider Observational Equivalence between Lazy Programs in Presence of Selective Strictness and Haeri later completed their work. Gabbay et al. and Haeri choose to manipulate the operational semantics of van Eekelen and de Mol to prevent increase in heap expressiveness upon expression evaluation. This improvement helped them to prove their desired observational equivalences using a novel proof technique called: Induction on the Number of Manipulated Bindings (INMB). They used (INMB) to prove a handful of interesting results including a couple of observational equivalences. However, their operational semantics suffers from restrictions in expressiveness.

In this talk, we investigate the elements in the operational semantics of Gabbay et al. and Haeri which cause restrictions in expressiveness. We present a new variation of van Eekelen and de Mol that, in the same time that retains all the interesting results in Gabbay et al. (including INMB), is as expressive as the operational semantics of van Eekelen and de Mol.

Conor McBride: Jockstrapping Dependent Types

Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coinci- dence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontriv- ial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article delivers a type-safe represen- tation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The KIPLING interpreter example is not merely de rigeur--- it is key to the construction. This is almost like bootstrapping, but at a higher level.

Chris Brown: Ever-Decreasing Circles: a Skeleton for Parallel Orbit Calculations in Eden.

The Orbit algorithm is widely used in symbolic computation, allowing the exploration of a solution space given some initial starting values and a number of mathematically-defined generators. In this paper, we consider how the Orbit algorithm can be encoded in Haskell, and thence how a parallel skeleton can be developed to cover a variety of Orbit calculations, using the Eden parallel dialect of Haskell. We report on a set of performance results that demonstrate the potential of the skeleton to allow a simple but effective implementation of the Orbit algorithm for shared-memory parallel machines.

Contact