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:
|