Good math/computation research (Was: HELP! formalizing OO)

Patrick Logan patrickl at servio.gemstone.com
Mon Apr 27 16:05:00 UTC 1998


    Could someone please point me to existing research in formalizing
    the OO approach (in relationship with fundamentals of Mathematics,
    Set Theory)?

I think there is a lot of good stuff happening in this area. Here are
a few of references I have found interesting in the past year or so...

(1) As someone else pointed out, Luca Cardelli has done work in this
    area. I like his slides "Everything is an Object" at
    http://www.luca.demon.co.uk

    This paper in particular compares the lambda calculus with a
    "calculus of objects" and shows how the former works as *more*
    fundamental than the latter.

The last two are not specific to object-oriented programming, per
se. But they address similar issues (modularization and encapsulation
of effects), and their paths are already converging with
object-oriented programming in the functional programming community:

(2) Eugenio Moggi developed the idea of a monad from category theory
    to combine descriptions of aspects computation. This has been
    adopted by Philip Wadler and many others in the functional
    programming community as a way to implement, rather than just
    describe, computation with "effects" (e.g. I/O, assignment, etc.)

    An interesting application of monads is building modular
    interpreters where each feature (I/O, continuations, exception
    handling, numbers, whatever.) is added or removed *without* having
    to change any of the other features.

    See http://www.cs.yale.edu/users/liang-sheng/thesis.ps.gz,
    "Modular Monadic Semantics and Compilation" and other papers in
    that directory.

(3) Girard (first name?) developed the idea of linear logic, which is
    a logic of resource usage. The idea is that a resource is
    consumed, and so it makes more sense to build that in to the rules
    of the logic than to attempt to describe resource usage via a
    logic where the same terms can be referenced over and over.

    This logic has been applied in a number of different ways to
    computation, because of the obvious connections. One interesting
    application of this is the language Clean which has "unique" types
    that can only be referenced once. Clean is available on Macs as
    well as Unix, Win32, etc. Programming the GUI is an example of
    using unique types. (For example, a window only appears once on
    the display, so it is a unique resource that is managed "cleanly"
    by a unique type.)

    Monads and linear objects are closely related. There are several
    papers that explore their relationships. Philip Wadler,
    http://netlib.bell-labs.com/cm/cs/who/wadler/index.html has
    advanced and introductory papers.

-- 
Patrick Logan                 mailto:patrickl at gemstone.com
Voice 503-533-3365            Fax   503-629-8556
Gemstone Systems, Inc         http://www.gemstone.com





More information about the Squeak-dev mailing list