[Pl-seminar] Reminder: 11/10: Mark P. Jones, "Habit: A Functional Language for Bare-metal Programming"

[Vincent St-Amour]

Reminder: The talk is in 25 minutes.

Vincent


At Wed, 02 Nov 2011 17:05:35 -0400,
Vincent St-Amour wrote:
> 
> NEU Programming Languages Seminar presents
> 
> Mark P. Jones
> The High Assurance Systems Programming Project (HASP)
> Department of Computer Science
> Portland State University, Portland, Oregon
> 
> *** NOTE: Non-Standard Time ***
> Thursday, 11/10
> 
> 11:00am - 1:00pm
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
> 
> Habit: A Functional Language for Bare-metal Programming
> 
> Several years ago, our group at Portland State began to explore the
> "crazy notion" of using Haskell---a high-level, purely functional
> language---for the development of operating systems components.
> This led to the development of a proof-of-concept demonstration
> system called "House", and more recently to a version of the L4
> microkernel, both implemented primarily in Haskell.  The results
> were encouraging, but also highlighted some weaknesses of Haskell in
> this particular domain, including not only the expected performance
> issues, but also the reliance on a large runtime system, and some
> difficulties in providing precise types for key low-level
> operations.
> 
> In this talk, we present the Habit programming language ("Haskell"+
> "bits"), which is inspired by Haskell, but designed more
> specifically to support the construction of bare-metal software.
> The overall design is fairly conservative---we have attempted to
> retain much of the familiarity and usability of Haskell---but we
> have also tried to address some of the weaknesses that we
> encountered in our earlier work.  Like Haskell, for example, Habit
> provides strong support for both functional and imperative styles of
> programming.  But it also differs by adopting a strict evaluation
> model, and by introducing new language features that include:
> mechanisms for fine control over representation of bit-level and
> memory-based data structures; a novel approach to initialization of
> memory areas; and a type system that allows precise characterization
> of size and layout information via type level naturals.
> 
> The talk will also describe the status of our prototype
> implementation, a novel aspect of which is the use of Leroy et al.'s
> Compcert framework in the backend as a step towards a long term goal
> of supporting certifying compilation of high-assurance, bare-metal
> software systems.
> 
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar