[PRL] Fwd: Conversations with Functional Programmers, Friday June 1, Harvard

[Mitchell Wand]

---------- Forwarded message ----------
From: Norman Ramsey <nr at eecs.harvard.edu>
Date: May 21, 2007 8:48 PM
Subject: Conversations with Functional Programmers, Friday June 1, Harvard
To: muller at cs.bc.edu, mairson at brandeis.edu, sk at cs.brown.edu,
church-advertise at types.bu.edu, hwxi at cs.bu.edu, Assaf Kfoury <kfoury at bu.edu>,
programming at eecs.harvard.edu, triforce at eecs.harvard.edu, dnj at csail.mit.edu,
mernst at csail.mit.edu, arvind at csail.mit.edu, will at ccs.neu.edu,
matthias at ccs.neu.edu, riccardo at ccs.neu.edu, shivers at ccs.neu.edu,
wand at ccs.neu.edu, david.chase at sun.com, victor.luchangco at sun.com,
Janwillem.Maessen at sun.com, sukyoung.ryu at sun.com, guy.steele at sun.com,
sguyer at cs.tufts.edu, fturbak at wellesley.edu
Cc: Hetchen Ehrenfeld <hetchen at deas.harvard.edu>

You are invited to join thirteen members of the ICFP program committee
and colleagues from around Boston for a short day of talks and
conversation about functional programming.  This informal meeting will
be atypical in two ways:

  * All the presenters will be experienced people presenting their own work.

  * You will have plenty of opportunity to interact with colleagues
    informally; I have aimed for every half-hour presentation to be
    complemented by a half-hour break.

Lunch will be served, provided you RSVP to Hetchen Ehrenfeld
<hetchen at deas.harvard.edu> by Tuesday, May 29.

Please circulate this invitation widely.


Norman Ramsey

             ***************** PROGRAM *****************

                 Friday, June 1, 10:00 AM to 4:30 PM
                 Maxwell-Dworkin G125 (ground floor)
                 33 Oxford Street
                 Harvard University

10:00-10:30 Nick Benton: Formalizing and Verifying Semantic
            Type Soundness of a Simple Compiler.

10:30-11:00 BREAK

11:00-11:30 Stephanie Weirich: Engineering Aspects of Formal Metatheory

11:30-12:00 BREAK

12:00-1:00  LUNCH --- please RSVP to hetchen at deas.harvard.edu

1:00-1:30  Mike Sperber: The Right Book isn't Enough
            (Progress for the Intro Course)

1:30-2:00  BREAK

2:00-2:30  Jeremy Gibbons: Generic and Indexed Programming

2:30-3:00  BREAK

3:00-3:30  Chris Stone: Computable Mathematics for Programmers

3:30-4:00  BREAK

4:00-4:30  Kevin Hammond: Hume and Multithreading


Location:
--------

Talks will take place in room G125 on the ground floor of Maxwell-
Dworkin.  An adjacent room with whiteboards will be available for
animated conversation.  Directions to Maxwell-Dworkin can be found at
http://www.eecs.harvard.edu/~nr/directions/harvard-via-t.html


            ***************** ABSTRACTS *****************

Nick Benton: "Formalizing and Verifying Semantic Type Soundness of a Simple
Compiler."

  We describe a semantic type soundness result, formalized in the Coq proof
  assistant, for a compiler from a simple imperative language with
  heap-allocated data into an idealized assembly language. Types in the
  high-level language are interpreted as binary relations, built using both
  second-order quantification and a form of separation structure, over
stores
  and code pointers in the low-level machine.


Jeremy Gibbons "Generic and Indexed Programming"
  (joint work with Bruno Oliveira and Meng Wang)

  The Generic and Indexed Programming project at Oxford
  started in November 2006, and is funded by EPSRC for three and a half
  years. The "generic" bit is about programs parametrized by datatypes,
  and builds on our work on the Datatype-Generic Programming project.
  This talk is about the "indexed" bit, which concerns lightweight
  techniques for dependently-typed programming, for example using
  generalized algebraic datatypes. Specifically, values are reflected
  at the type level, and can then be used as "phantom type" indices to
  other types, expressing certain kinds of constraints; the
  relationship between type representations and values, important in
  datatype-generic programming, is one application. We will explain our
  motivation, show some cool examples, and say a little about where we
  see the project going.


Mike Sperber: The Right Book isn't Enough: Progress for the Intro Course

  The work of Felleisen's TeachScheme! has shown what constitutes good
  material in an introductory programming course.  While the TeachScheme!
  approach has been successfully implemented by many high schools and
  universities, just following its guidance isn't enough to ensure a good
  learning experience for the students.  Teaching the intro course
  continues to be extraordinarily difficult because it is very easy for
  the teaching team to misconstrue an enjoyable teaching experience as a
  successful learning experience for the students, which is often not the
  case.  An understanding of what motivates students, and close, continued
  observation of their learning habits are necessary to ensure that actual
  learning takes place.  The talk reports on experience gained teaching
  the intro course at University of Tübingen since 1999.


Stephanie Weirich: Engineering Aspects of Formal Metatheory.
  (joint work with Brian Aydemir, Arthur Charguéraud, and Benjamin C.
Pierce)

  Machine-checked proofs of the properties of programming languages have
  become a critical need, both for increasing confidence in large and
  complex designs and as a foundation for technologies such as
  proof-carrying code. However, constructing these proofs remains a black
  art, involving many choices in the formulation of basic definitions
  that are commonly elided in informal arguments but that make a huge
  cumulative difference in the difficulty of carrying out large
  developments formally.

  To clarify these basic choices, we have constructed reference
  formalizations in Coq of type soundness for several core programming
  languages-the simply-typed lambda calculus, System F-sub, and
  mini-ML-and subject-reduction for the Calculus of Constructions. No
  single aspect of these formalizations is especially novel; our goal,
  rather, has been to assemble a good set of mutually supporting design
  choices, together with a small number of powerful tactics to make
  proofs in this domain as smooth and natural as possible. Key features
  include a locally nameless representation for syntax with binders, a
  formulation of the 'local closure' predicate that leads to a natural
  induction principle for terms, and a treatment of variable freshness
  using universal quantification over a cofinite set of names.


Chris Stone: RZ: Computable Mathematics for Programmers
  (joint work with Andrej Bauer)

  The RZ system is a lightweight tool for translating mathematical
  specifications in constructive logic into ML signatures with classical
  assertions. Constructive mathematics involves some seemingly puzzling
  concepts
  (such as a finite set without a size). But these can become much more
  intelligible when translated into the language understood by
  programmers.

  In this talk I will show some examples, briefly summarize the the design
  of the translator, and discuss the suitability of ML as our target
  language.


Kevin Hammond: Hume and Multithreading

  Hume is a novel language combining finite-state-automaton ideas (for
  concurrency) with purely functional programming (for computations).
  The language is structured as a series of levels, where each higher
  level gains in abstraction, but increases the difficulty of providing
  accurate cost information and other properties.  We have built formal
  cost models for various levels of Hume from a simple notation targeted
  as a hardware description language, through to a sophisticated
  notation including recursion, user-defined inductive data structures,
  exceptions and other language constructs which is intended as a near
  general-purpose language.


  Based on our experience with multithreaded computations on the Grip
  research architecture of the 1980s, we believe that the Hume design
  will help us expose clearly delimited *and independent* fine-grained
  parallel computations that should meet the requirements of modern
  micro-architectures, and in which the cost information we will provide
  important scheduling hooks.  This talk will present Hume and discuss
  connections with micro-architectures


           ***************** BONUS TOPICS *****************

What are you to do with all this break time?  Whatever you like,
really, but you might like to ask our visitors about some other things
they are working on, listed here.


Jeremy Gibbons: "Parametric Datatype-Genericity"
  (joint work with Ross Paterson)

  Datatype-generic programs are programs parametrized by a
  datatype or type functor. There are two main styles of datatype-
  generic programming: the Algebra of Programming approach,
  characterized by structured recursion operators parametrized by a
  shape functor, and the Generic Haskell approach, characterized by
  case analysis over the structure of a datatype. We show that the
  former enjoys a kind of parametricity, relating the behaviours of
  generic functions at different types; in contrast, the latter is more
  ad hoc, with no coherence required or provided between the various
  clauses.


Mike Sperber: Age and Tractability: Scheme 48 through the Years

  Scheme 48 is a substantial Scheme system that has been around for over
  20 years.  Despite its substantial functionality, it has maintained
  tractability, one of its most important design goals.  Tractability has
  been achieved through rigorous modularization and determined re-use of
  central system components.  In particular, Scheme 48 has recently
  acquired an optimizing native-code compiler, large parts of which were
  re-used from previously existing components.  The talk gives an overview
  of the state of the system (particularly the optimizing native-code
  compiler), how it is different from other systems, and how re-use and
  modularization have affected its development.

Mike Sperber: It's All about Being Right: Lessons from the R6RS Process

  In the Revised Reports on Scheme up to R5RS, the language could only be
  changed by unanimous consent. It has been widely believed that any
  language changes made in this way would clearly be the right
  thing. Arguably, this process reached its limits with the Revised5
  Report on Scheme: Crucial language additions such as modules, records
  and exceptions had little chance of reaching unamimous consent, no
  matter what the specific design. While the editors of the Revised6
  Report no longer follow this rule, standardization is still driven by a
  strong desire to do the right thing. Continuing the tradition of Lisp
  culture, reaching this goal has been difficult and elusive, as the
  participants hold different and strongly opinionated ideas about what
  the right thing is. In the talk, I will review the R6RS process, and
  attempt to show that R6RS is indeed the right thing for Scheme.
-------------- next part --------------
HTML attachment scrubbed and removed