[PRL] torture chamber Wed | 11:45 | 366

[Dale Vaillancourt]

PRL,

I will be practicing my ACL2 Workshop talk on Wednesday (8/9) at  
11:45 in 366 (the usual PL Seminar  slot).  Please come and  
participate in the torture!

Abstract:

Teaching undergraduates to develop software in a formal framework  
such as
ACL2 poses two immediate challenges. First, students typically do not  
know
applicative programming and are often unfamiliar with ACL2's
syntax. Second, for motivational reasons, students prefer to work on
projects that involve designing interactive, graphical applications.

In this paper, we present Dracula, a pedagogic programming environment
that partially solves these problems. The environment adds a subset of
Applicative Common Lisp to DrScheme, an integrated programming  
environment
for Scheme. Dracula thus inherits DrScheme's
pedagogic capabilities, especially its treatment of syntax and run-time
errors. Further, Dracula also comes with a library for
programming interactive, graphical games.  The library interface forces
students to think of a graphical user interface in terms of
state-transition functions, enabling them later to prove theorems about
their games in ACL2. Dracula{} provides a graphical front-end to
the ACL2 theorem prover for this purpose.  In short, Dracula allows the
formulation of student projects that represent an important intermediate
point between data structure exercises in theorem proving and
industrial applications.

-Dale

P.S.  My talk will not consume the whole PL Seminar slot.  If you  
would like to be tortured after me, feel free to schedule yourself in  
the same block.