Lambda the Ultimate

Another draft entry for HOPL-III about the The Development of the Emerald Programming Language by Andrew P. Black, Norman Hutchinson, Eric Jul and Henry M. Levy.

Emerald is an object-based programming language and system designed and implemented in the Department of Computer Science at the University of Washington in the early and mid-1980s. The goal of Emerald was to simplify the construction of distributed applications. This goal was re- flected at every level of the system: its object structure, the programming language design, the compiler implementation, and the run-time support.

This paper describes the origins of the Emerald group, the forces that formed the language, the influences that Emerald has had on subsequent distributed systems and programming languages, and some of Emerald’s more interesting technical innovations.

Worth a read for those interested in PL research topics which are still in play. Emerald explored a number of topics including distributed programming in the presence of failure; Mobile objects; Active objects; structural typing (as opposed to nominal); Static typing in the presence of open programming (shades of the ongoing work in Alice ML); Parametirized types. All of this while having performance as a top priority.

Previous links to HOPL-III papers.

I wrote an essay titled "Thoughts about the Best Introductory Language which discusses the suitability of various languages as introductory programming languages, covers several approaches to that, explains why they are wrong or right, etc. I believe the final conclusion is less important than the actual insights and discussion presented there.

Read, share, comment and enjoy!

A Logic for Parametric Polymorphism, Gordon Plotkin and Martín Abadi.

In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simply-typed lambda-calculus with recursion and arithmetic, our logic is a logic for System F. The logic permits the formal presentation and use of relational parametricity. Parametricity yields --- for example --- encodings of initial algebras, final co-algebras and abstract datatypes, with corresponding proof principles of induction, co-induction and simulation.