[TYPES/announce] Call for Participation: Scheme & Functional Programming Workshop 2006

[Robby Findler]

Dear all,

The Scheme and Functional Programming Workshop
pre-registration deadline is in about 2 and a half weeks --
do be sure to register for ICFP and the workshop before
then.

Come to hear Manuel Serrano talk about HOP, his new language
for programming the web, a status report from the R6RS
editors, and presentations of the work below. I look forward
to seeing you in Portland!

  http://scheme2006.cs.uchicago.edu/

Best,
Robby

========================================

A Self-Hosting Evaluator using HOAS
Eli Barzilay (Northeastern University)

We demonstrate a tiny, yet non-trivial evaluator that is
powerful enough to run practical code, including
itself. This is made possible using a Higher-Order Abstract
Syntax (HOAS) representation -- a technique that has become
popular in syntax-related research during the past
decade. With a HOAS encoding, we use functions to encode
binders in syntax values, leading to an advantages of
reflecting binders rather than re-implementing them.

In Scheme, hygienic macros cover problems that are
associated with binders in an elegant way, but only when
extending the language, i.e., when we work at the
meta-level. In contrast, HOAS is a useful object-level
technique, used when we need to represent syntax values that
contain bindings -- and this is achieved in a way that is
simple, robust, and efficient. We gradually develop the
code, explaining the technique and its benefits, while
playing with the evaluator.


>From Variadic Functions to Variadic Relations
William E. Byrd and Daniel P. Friedman (Indiana University)

Scheme makes it easy to define variadic functions, which
take an arbitrary number of arguments; miniKanren, a logic
programming language embedded in R5RS Scheme, makes it easy
to define variadic relations. A variadic miniKanren relation
takes two arguments: a list containing input arguments and
an output argument. A fresh or partially-instantiated logic
variable passed to a variadic relation can represent the
list of input arguments. A relation may also be
super-variadic---such a relation takes a list of lists of
input arguments.

We show the variadic and super-variadic relational
equivalent of several variadic functions, examples of their
use, and several abstractions over these relations. We also
present a brief miniKanren overview, along with an
R5RS-compliant implementation of the subset of miniKanren
that we use.


Experiences with Scheme in an Electro-Optics Laboratory
Richard Cleis and Keith Wilson (Air Force Research Laboratory)

The Starfire Optical Range is an Air Force Research
Laboratory engaged in Atmospheric Research near Albuquerque,
New Mexico. Since the late 1980's it has developed numerous
telescope systems and auxiliary devices. Nearly all are
controlled by C programs that became difficult to manage due
to the large number of configurations required to support
the experiments. To alleviate the problem, Scheme has been
introduced in at least six distinct ways. This paper
describes the uses of Scheme, emerging programming
techniques, and general experiences of the past several
years.


Rapid Case Dispatch in Scheme
William D. Clinger (Northeastern University)

The case expressions of Scheme can and should be implemented
efficiently. A three-level dispatch performs well, even when
dispatching on symbols, and scales to large case
expressions.


A Stepper for Scheme Macros
Ryan Culpepper, Matthias Felleisen (Northeastern University)

Even in the days of Lisp's simple defmacro systems, macro
developers did not have adequate debugging support from
their programming environment. Modern Scheme macro expanders
are more complex than Lisp's, implementing lexical hygiene,
referential transparency for macro definitions, and
frequently other source properties. Scheme implementations,
however, have only adapted Lisp's inadequate macro
inspection tools. Unfortunately, these tools rely on a
rather naive model of the expansion process, thus leaving a
large gap between Scheme's complex mode of expansion and
what the programmer sees.

In this paper, we present a macro debugger with full support
for modern Scheme macros. To construct the debugger, we have
extended the macro expander so that it issues a series of
expansion events. A parser turns these event streams into
derivations in a natural semantics for macro expansion. From
these derivations, the debugger extracts a
reduction-sequence (stepping) view of the expansion. A
programmer can specify with simple policies which parts of a
derivation to omit and which parts to show. Last but not
least, the debugger includes a syntax browser that
graphically displays the various pieces of information
attached to syntactic tokens.


Automatic construction of parse trees for lexemes
Danny Dub\'e (Universit\'e Laval) and Anass Kadiri (EPITA, Paris France)

Recently, Dub\'e and Feeley presented a technique that makes
lexical analyzers able to build parse trees for the lexemes
that match regular expressions. While parse trees usually
demonstrate how a word is generated by a context-free
grammar, these parse trees demonstrate how a word is
generated by a regular expression, in an analogous
fashion. This paper describes the adaptation and
implementation of that technique in a concrete lexical
analyzer generator. The adaptation of the technique includes
extending it to the rich set of operators handled by the
generator and reversing the direction of the parse trees
construction so that it corresponds to the natural
right-to-left direction of the Scheme lists
construction. The implementation of the adapted technique
includes modifications to both the generation-time and the
run-time parts of the generator. Uses of the new addition
and empirical measurements of its cost are
presented. Extensions and alternatives to the technique are
considered.


Concurrency Oriented Programming in Termite Scheme 
Guillaume Germain, Marc Feeley, Stefan Monnier (Universit\'e de Montr\'eal)

Termite is a language and system offering a simple and
powerful tool for expressing distributed computation. It is
based on a message-passing model of concurrency inspired by
Erlang, and on a variant of the functional language Scheme.

Our system is an appropriate tool for building custom
protocols and abstractions for distributed computation. Its
open network model allows for the building of
non-centralized distributed applications. The possibility of
failure is reflected in the model, and ways to handle them
are proposed. The existence of first-class continuations is
exploited in order to allow the expression of high-level
concepts such as migration of processes.

We describe the Termite model with its implications and
describe sample applications built with Termite. We conclude
with a discussion of the current implementation and its
performance.


An Incremental Approach to Compiler Construction
Abdulaziz Ghuloum (Indiana University)

Compilers are perceived to be magical artifacts, carefully
crafted by the wizards, and unfathomable by the mere
mortals. Books on compilers are better described as
wizard-talk: written by and for a clique of all-knowing
practitioners. Real-life compilers are too complex to serve
as an educational tool. And the gap between real-life
compilers and the educational toy compilers is too wide. The
novice compiler writer stands puzzled facing an impenetrable
barrier, ``better write an interpreter instead.''

The goal of this paper is to break that barrier. We show
that building a compiler can be as easy as building an
interpreter. The compiler we construct accepts a large
subset of the Scheme programming language and produces
assembly code for the Intel-x86 architecture, the dominant
architecture of personal computing. The development of the
compiler is broken into many small incremental steps. Every
step yields a fully working compiler for a progressively
expanding subset of Scheme. Every compiler step produces
real assembly code that can be assembled then executed
directly by the hardware. We assume that the reader is
familiar with the basic computer architecture: its
components and execution model. Detailed knowledge of the
Intel-x86 architecture is not required.

The development of the compiler is described in detail in an
extended tutorial. Supporting material for the tutorial such
as an automated testing facility coupled with a a
comprehensive test suite are provided with the tutorial. It
is our hope that current and future implementors of Scheme
find in this paper the motivation for developing
high-performance compilers and the means for achieving that
goal.


Sage: Hybrid Checking for Flexible Specifications
Jessica Gronski (University of California, Santa Cruz
(UCSC)), Kenneth Knowles (UCSC), Aaron Tomb (UCSC), Stephen
N. Freund (Williams College), and Cormac Flanagan (UCSC)

Software systems typically contain large APIs that are
informally specified and hence easily misused. This paper
presents the Sage programming language, which is designed to
enforce precise interface specifications in a flexible
manner. The Sage type system uses a synthesis of the type
``dynamic'', first-class types, and arbitrary refinement
types. Since type checking for this expressive language is
not statically decidable, Sage uses hybrid type checking,
which extends static type checking with dynamic contract
checking, automatic theorem proving, and a database of
refuted subtype judgments.


Interaction-Safe State for the Web
Jay McCarthy and Shriram Krishnamurthi (Brown University)

Recent research has demonstrated that continuations provide
a clean basis to describe interactive Web programs. This
account, however, provides only a limited description of
state, which is essential to several Web applications. This
state is affected by the numerous control operators (known
as navigation buttons) in Web browsers, which make Web
applications behave in unexpected and even erroneous ways.

We describe these subtleties as discovered in the context of
working Web applications. Based on this analysis we present
linguistic extensions that accurately capture state in the
context of the Web, presenting a novel form of dynamic
scope. We support this investigation with a formal semantics
and a discussion of applications. The results of this paper
have already been successfully applied to working
applications.


Component Deployment with PLaneT: You Want it Where?
Jacob Matthews (University of Chicago)

For the past two years we have been developing PLaneT, a
package manager built into PLT Scheme's module system that
simplifies program development by doing away with the
distinction between installed and uninstalled packages. In
this paper we explain how PLaneT works and the rationales
behind our major design choices, focusing particularly on
our decision to integrate PLaneT into PLT Scheme and the
consequences that decision had for PLaneT's design. We also
report our experience as PLaneT users and developers and
describe what have emerged as its biggest advantages and
drawbacks.


Scheme for Client-Side Scripting in Mobile Web Browsing, or
AJAX-Like Behavior Without Javascript
Ray Rischpater (Rocket Mobile, Inc.)

I present an implementation of Scheme embedded within a Web
browser for wireless terminals. Based on a port of
TinyScheme integrated with RocketBrowser, an XHTML-MP
browser running on Qualcomm BREW-enabled handsets, the
resulting application can support the same use cases as
traditional JavaScript-enabled browsers, including
asynchronous programming recently popularized via AJAX
(Asynchronous Javascript and XML). In addition to a
comparison of the resulting script capabilities, I present
the changes required to bring TinyScheme to Qualcomm BREW,
including adding support for BREW components as TinyScheme
data types.


SHard: a Scheme to Hardware Compiler
Xavier Saint-Mleux (Universit\'e de Montr\'eal), Marc Feeley
(Universit\'e de Montr\'eal) and Jean-Pierre David (\'Ecole
Polytechnique de Montr\'eal)

Implementing embedded systems in hardware can have several
benefits (performance, power usage, etc.). Current
hardware/software co-design methodologies, which offer a
language for describing hardware and another language for
programming the software, put the burden of system
partitioning on the developer, which is tedious and makes
component transformation and reuse difficult. Our goal is to
put most of this burden on the compiler through the use of a
single, simple programming language. We describe a prototype
compiler that compiles a functional subset of Scheme into a
high-level description of dataflow parallel hardware. The
compiler supports tail and non-tail function calls and
higher-order functions. Our approach makes it possible to
implement software algorithms in hardware with very few
modifications (e.g. IO channel declaration). Performance
results of our system are given for FPGA hardware.


Gradual Typing for Functional Languages
Jeremy G. Siek and Walid Taha (Rice University)

Static and dynamic type systems have well-known strengths
and weaknesses, and each is better suited for different
programming tasks. There have been many efforts to integrate
static and dynamic typing and thereby combine the benefits
of both typing disciplines in the same language. The
flexibility of static typing can be improved by adding a
type Dynamic and a typecase form. The safety and performance
of dynamic typing can be improved by adding optional type
annotations or by performing type inference (as in soft
typing). However, there has been little formal work on type
systems that allow a programmer-controlled migration between
dynamic and static typing. Thatte proposed Quasi-Static
Typing, but it does not statically catch all type errors in
completely annotated programs. Anderson and Drossopoulou
defined a nominal type system for an object-oriented
language with optional type annotations. However, developing
a sound, gradual type system for functional languages with
structural types is an open problem.

In this paper we present a solution based on the intuition
that the structure of a type may be partially known/unknown
at compile-time and the job of the type system is to catch
incompatibilities between the known parts of types. We
define the static and dynamic semantics of a lambda-calculus
with optional type annotations and we prove that its type
system is sound with respect to the simply-typed
lambda-calculus for fully-annotated terms. We prove that
this calculus is type safe and that the cost of dynamism is
``pay-as-you-go''.