| Dr. John Maraist | |
|
I have moved to New Orleans, and am no longer affiliated with DePaul. I can be reached at the email address depaul-stuff at the host maraist dot org . My personal web pages are located at maraist.org. The rest of this page is an archive of work at the time I left DePaul. |
|
| Research and selected publications | |
|
On classical linear logic and its lambda calculus
|
(1999) The main idea is a natural deduction system and
lambda calculus for full, classical linear logic.
(There are also decorations of the Schellinx
translations from the usual lambda calculi into this
system, corresponding to call-by-name and by-value,
although it turned out that Ichiro Ogata had done
more-or-less the same sort of thing, looking at LKQ and
LKT, a few months before.) This work is described in
Technical Report ACRC/00/014 from the Advanced Computing
Research Centre of the University of South Australia
(ask the School's
secretary to mail you a hard copy).
|
|
On the lambda calculus and minimal intuitionistic
linear logic
|
(1996) The motivating idea of this work was that one can
better compare different ways of reducing terms in the
lambda calculus by mapping different reduction
strategies in different ways into a single third
system. The standard example from the distant past is
Plotkin's two continuation passing transforms for
call-by-name and call-by-value reduction. After the
appropriate transformation, each reduction order can
simulate the other; in fact, the order is no longer
relevant. There is a journal
paper (with Odersky, Wadler and Turner) describing
the translation of call-by-name and call-by-value into a
linear lambda calculus, and call-by-need into an affine
calculus; and a conference
paper describing how all three calling conventions
can be mapped into a single system with separate modes
for weakening and contraction. My doctoral thesis is also
about this sort of thing.
|
|
On the call-by-need lambda calculus
|
(1994) The intuitive idea of the call-by-need lambda
calculus is to capture both the property of the
call-by-name calculus that only needed terms are reduced
and the call-by-value behavior that only values are
copied. Moreover, call-by-need operates only on terms,
without requiring a separate heap of bindings, which can
make reasoning with it simpler. There is a journal paper (with Odersky and
Wadler).
|
|
On design patterns
|
(1997) Design patterns allow common programming idioms
to be re-used from implementation to
implementation. With Chris Salzmann, a master's student
from the University of Karlsruhe, we have explored the
use of design patterns to design self-extendible
systems. Chris designed and implemented a prototype in
the Pizza programming language,
which he'll release after he gets a chance to clean up
the code. Our experience with the design is summarized
in the paper below. There is a conference paper (with
Salzmann).
|
|
On compiling functional-logic programming languages
|
(1994) Implementations of logic languages, generally
speaking, have some sort of computational step which
allows reconsideration of previous decisions to bind
certain quantifiers to certain identifiers, usually some
sort of backtracking. Functional logic languages -
again, generally speaking - augment the reduction
semantics of functional languages with the backtracking
mechanism of logic languages. This work describes an
implimentation technique called quasisharing which
allows information computed in one branch of a search to
be reused when relevant after backtracking into a new
branch. The technique resembles Lamping's strategy for
optimal lambda reduction. There is a conference paper focusing on
the design and the graph calculus, and a workshop paper that discusses
the abstract machine (both with Silbermann). My master's thesis is also
about this topic.
|
|
There is also a BibTeX file with
entries for the above papers, their abstracts, and
various other superseded earlier papers on those topics.
Just about everything here is also mirrored on the Hypatia
archive, based in England, which may be useful to
know if this site is giving you trouble. Another nice
site for research in CS is the NEC research
index, which is a citation index but which also
seems to have some pointers to papers (my
entry there).
|
|
|
Code |
|
|
LaTeX code
|
For my thesis I wrote a package which accumulates the
page numbers on which each bibliographic entry is cited,
and provides an interface command which allows the page
list for each label to be included in the
document. N.B.: there is no interface yet for BibTeX;
the code is a TeX/LaTeX package only.
|
|
Elisp modes
|
Some time ago I wrote a number of Elisp packages. Package extraregional.el separates the notions of point, mark and region from the notion of selection. The idea is that, usually in a different window, you should be able to select text without affecting the selected window, the current buffer or the values of point at the various windows and buffers. Version 0.2 is a rather smaller package than version 0.1.1: I found that the extras were not really all that useful, and were actually pretty fragile. The older version is still available, although it does not work under Xemacs version 19.3. Package rmail-labelsorter.el makes labels a little bit easier to handle in Rmail. The code is usable as it is, but is not documented - this situation probably won't change, as I no longer use rmail. Caveat emptor. |
|
|