Ivory is a language that enforces memory safety and avoids most undefined behaviors while providing low-level control of memory- manipulation. Ivory is embedded in a modern variant of Haskell, as implemented by the GHC compiler. The main contributions of the paper are two-fold. First, we demonstrate how to embed the type-system of a safe-C language into the type extensions of GHC. Second, Ivory is of interest in its own right, as a powerful language for writing high-assurance embedded programs. Beyond invariants enforced by its type-system, Ivory has direct support for model-checking, theorem-proving, and property-based testing. Ivory’s semantics have been formalized and proved to guarantee memory safety.

We report on our experiences in synthesizing a fully-featured autopilot from embedded domain-specific languages (EDSLs) hosted in Haskell. The autopilot is approximately 50k lines of C code generated from 10k lines of EDSL code and includes control laws, mode logic, encrypted communications system, and device drivers. The autopilot was built in less than two engineer years. This is the story of how EDSLs provided the productivity and safety gains to do large-scale low-level embedded programming and lessons we learned in doing so.

Secure multiparty computation (SMC) permits a collection of parties to compute a collaborative result, without any of the parties gaining any knowledge about the inputs provided by other parties. Specifications for SMC are commonly presented as boolean circuits, where optimizations come mostly from reducing the number of multiply-operations (including and-gates) - these are the operations which incur significant cost, either in computation overhead or in communication between the parties. Instead, we take a language-oriented approach, and consequently are able to explore many other kinds of optimizations. We present an efficient and general purpose SMC table-lookup algorithm that can serve as a direct alternative to circuits. Looking up a private (i.e. shared, or encrypted) n-bit argument in a public table requires log(n) parallel-and operations. We use the advanced encryption standard algorithm (AES) as a driving motivation, and by introducing different kinds of parallelization techniques, produce the fastest current SMC implementation of AES, improving the best previously reported results by well over an order of magnitude.

Even though step-by-step refinement has long been seen as desirable, it is hard to find compelling industrial applications of the technique. In theory, transforming a high-level specification into a high-performance implementation is an ideal means of producing a correct design, but in practice it is hard to make it work, and even harder to make it worthwhile. This talk describes an exception.

We present a concurrent scripting language embedded in Haskell, emulating the functionality of the Orc orchestration language by providing many-valued (real) non-determinism in the context of concurrent effects. We provide many examples of its use, as well as a brief description of how we use the embedded Orc DSL in practice. We describe the abstraction layers of the implementation, and use the fact that we have a layered approach to demonstrate algebraic properties satisfied by the combinators.

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, except that our business lacked focus. Every new job had to be found and sold from scratch. We realized that we had to focus on a specific market if we wanted to achieve stability and growth. We chose High Assurance Software as it was a natural fit both for our technology and our expertise, further narrowing our attention to information assurance (IA).

Certain programs making use of monads need to perform recursion over the values of monadic actions. Although the do-notation of Haskell provides a convenient framework for monadic programming, it lacks the generality to support such recursive bindings. In this paper, we describe an enhanced translation schema for the donotation and its integration into Haskell. The new translation allows variables to be bound recursively, provided the underlying monad comes equipped with an appropriate fixed-point operator.

Monads have become a popular tool for dealing with computational effects in Haskell for two significant reasons: equational reasoning is retained even in the presence of effects; and program modularity is enhanced by hiding "plumbing" issues inside the monadic infrastructure. Unfortunately, not all the facilities provided by the underlying language are readily available for monadic computations. In particular, while recursive monadic computations can be defined directly using Haskell's built-in recursion capabilities, there is no natural way to express recursion over the values of monadic actions. Using examples, we illustrate why this is a problem, and we propose an extension to Haskell's donotation to remedy the situation. It turns out that the structure of monadic value-recursion depends on the structure of the underlying monad. We propose an axiomatization of the recursion operation and provide a catalogue of definitions that satisfy our criteria.

This paper introduces a language feature, called implicit parameters, that provides dynamically scoped variables within a statically-typed Hindley-Milner framework. Implicit parameters are lexically distinct from regular identifiers, and are bound by a special with construct whose scope is dynamic, rather than static as with let. Implicit parameters are treated by the type system as parameters that are not explicitly declared, but are inferred from their use.

Based on our experience with modelling and verifying microarchitectural designs within Haskell, this paper examines our use of Haskell as host for an embedded language. In particular, we highlight our use of Haskell's lazy lists, type classes, lazy state monad, and unsafe Perform I0, and point to several areas where Haskell could be improved in the future. We end with an example of a benefit gained by bringing the functional perspective to microarchitectural modelling.

Compilers for ML and Haskell use intermediate languages that incorporate deeply-embedded assumptions about order of evaluation and side effects. We propose an intermediate language into which one can compile both ML and Haskell, thereby facilitating the sharing of ideas and infrastructure, and supporting language developments that move each language in the direction of the other. Achieving this goal without compromising the ability to Compile as good code as a more direct route turned out to be much more subtle than we expected. We address this challenge using monads and unpointed types, identify two alternative language designs, and explore the choices they embody.

No abstract available.

Type safety of imperative programs is an area fraught with difficulty and requiring great care. The SML solution to the problem, originally involving imperative type variables, has been recently simplified to the syntactic-value restriction. In Haskell, the problem is addressed in a rather different way using explicit monadic state. We present an operational semantics for state in Haskell and the first full proof of type safety. We demonstrate that the semantic notion of value provided by the explicit monadic types is able to avoid any problems with generalization.

Abstract The projection-based strictness analysis of Wadler and Hughes is elegant and theoretically satisfying except in one respect: the need for lifting. The domains and functions over which the analysis is performed need to be transformed, leading to a less direct correspondence between analysis and program than might be hoped for. In this paper we shall see that the projection analysis may be reformulated in terms of partial projections, so removing this infelicity. There are additional benefits of the formulation: the two forms of information captured by the projection are distinguished, and the operational significance of the range of the projection fits exactly with the theory of unboxed types.

Depth-first search is the key to a wide variety of graph algorithms. In this paper we express depth-first search in a lazy functional language, obtaining a linear-time implementation. Unlike traditional imperative presentations, we use the structuring methods of functional languages to construct algorithms from individual reusable components. This style of algorithm construction turns out to be quite amenable to formal proof, which we exemplify through a calculational-style proof of a far from obvious strongly-connected components algorithm.

Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language.

We define an operational semantics for lazy evaluation which provides an accurate model for sharing. The only computational structure we introduce is a set of bindings which corresponds closely to a heap. The semantics is set at a considerably higher level of abstraction than operational semantics for particular abstract machines, so is more suitable for a variety of proofs. Furthermore, because a heap is explicitly modelled, the semantics provides a suitable framework for studies about space behaviour of terms under lazy evaluation.

We apply the categorical properties of polymorphic functions to compile-time analysis, specifically projection-based strictness analysis. First we interpret parameterised types as functors in a suitable category, and show that they preserve monics and epics. Then we define “strong” and “weak” polymorphism, the latter admitting certain projections that are not polymorphic in the usual sense. We prove that, under the right conditions, a weakly polymorphic function is characterised by a single instance. It follows that the strictness analysis of one simple instance of a polymorphic function yields results that apply to all. We show how this theory may be applied. In comparison with earlier polymorphic strictness analysis methods, ours can apply polymorphic information to a particular instance very simply. The categorical approach simplifies our proofs, enabling them to be carried out at a higher level, and making them independent of the precise form of the programming language to be analysed. The major limitation of our results is that they apply only to first-order functions.

article Free Access Share on Strictness and binding-time analyses: two for the price of one Author: John Launchbury University of Glasgow University of GlasgowView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 6June 1991 pp 80–91https://doi.org/10.1145/113446.113453Online:01 May 1991Publication History 9citation234DownloadsMetricsTotal Citations9Total Downloads234Last 12 Months8Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

In this paper, we describe a method by which language parsers and interpreters may be implemented in a lazy functional programming language. The visual appearance of such interpreters mimics the BNP description of the grammar of the language being interpreted. The method is particularly well suited to the implementation of language interpreters that are based on the principle of ‘rule to rule’ correspondence (in which each production rule of the grammar has a translation rule associated with it). The main objective of the paper is to demonstrate that the method described provides a useful framework within which both grammars and semantic theories of languages many be investigated. We present the method by example: the simple natural language interpreter we construct is based loosely on principles proposed by Richard Montague.