Programming Wednesdays Talks

  • Implementation and Evaluation of a Safe Runtime in Cyclone (Feb. 18, 2004) 20040218-HarvardPL1.ppt 20040218-HarvardPL2.ppt

    In this talk we outline the implementation of a simple Scheme interpreter and a copying garbage collector that manages the memory allocated by the interpreter. The entire system including the garbage collector is implemented in Cyclone, a safe dialect of C, which supports safe and explicit memory management. We describe the high-level design of the system, report preliminary benchmarks, and compare our approach to other Scheme systems. Our preliminary benchmarks demonstrate that one can build a system with reasonable performance when compared to other approaches that guarantee safety. More importantly we can significantly reduce the amount of unsafe code needed to implement the system. Our benchmarks also identify some key algorithmic bottlenecks related to our approach that we hope to address in the future.

    Although most of the theoretical ideas in this work are not by themselves novel, there are a few interesting variations and combinations of the existing literature we will discuss. However, the primary motivation and goal is to build a realistic working system that puts all the existing theory to test against existing systems which rely on larger amounts of unsafe code in their implementation.

  • L3: A Linear Language with Locations (Oct. 20, 2004) 20041020-HarvardPL.pdf

    We present a simple, but expressive type system that supports strong updates --- updating a memory cell to hold values of unrelated types at different points in time. Our formulation is based upon standard linear logic and, as a result, enjoys a simple semantic interpretation for types that is closely related to models for spatial logics. The typing interpretation is strong enough that, in spite of the fact that our core calculus supports shared, mutable references and cyclic graphs, every well-typed program terminates.

    We then consider extensions needed to model ML-style references, where the capability to access a reference cell is unrestricted, but strong updates are disallowed. Our extensions include a thaw primitive for re-gaining the capability to perform strong updates on unrestricted references. The thaw primitive is closely related to other mechanisms that support strong updates, such as CQual's restrict.

  • The MLton Standard ML Compiler (Dec. 1, 2004) http://www.mlton.org/Talk

    I will be talking about MLton -- an open-source, whole-program, optimizing Standard ML compiler. Given the topics covered in this group over the last couple of weeks (an optimization framework, a debugging framework), it seems timely to look at a full-blown compiler. I'll give an overview of MLton (some philosophy, history, etc.) before taking a closer look at the optimization passes. And, I won't be pulling any punches: the whole talk will be delivered from the mlton.org website with direct links into the CVS repository. Want to see where a body is buried? We'll dig it up!

  • Discussion on The Big Programming Issue (Mar. 9, 2005)

    Two articles stood out as good discussion starters:

    I suggest everyone read with an open mind: the articles are very much written in a "popular science" manner. But, I think they make good starting points for questions like: Who are the consumers of PL research? What are the far reaching visions for PL? What are the popular perceptions of PL?

  • A Guided Tour to a Twelf Proof (July 6, 2005 and July 20, 2005) 20050706-HarvardPL.pdf

    I've recently completed a "proof" in Twelf of type-safety for a substructural, lambda-calculus. There are certainly members of our research group that are interested in being walked through such a development, and we are inviting anyone else who might find it interesting.

    A few more details for those interested:

    One part of the motivation for this was the POPLMark challenge and the Twelf solution. A couple of months ago, there was a lot of discussion on the POPLMark mailing list that really put forward a lot of good reasons that Twelf could be the way of formalizing programming languages proofs, particularly type safety proofs.

    Having been so convinced, I'm naturally led to try out Twelf for my own work, which has recently been trying to apply substructural type systems (a fine-grained refinement of linear type systems) to "tame" state and effects. While the proof I completed does not come close to being a proof a feature-complete language, it does shed some light on what it would take to scale up to more features. I believe that it also highlights some of the strengths and weakenesses of Twelf in this domain.

    The type safety proof is essentially covers the language presented in Section 1.2 of the "Substructural Type Systems" chapter (by David Walker) in Advanced Topics in Types and Programming Languages.

    Additional Resources: