Previous ML Club Meetings 1998-99

  • 1998:
  • 19th Feb. John Longley
    A possible extension to ML based on games and strategies
    I would like to talk about a recent idea concerning a possible extension to an ML-like language. (This is different from, and possibly more useful than, the kind of extension I talked about at various times last year.) The language feature in question seems to have the same expressive power as exceptions in some theoretical sense, but (I believe) allows certain tasks to be performed much more efficiently than is currently possible in ML. The idea was inspired partly by theoretical work in game semantics, and partly by my attempts to design an efficient algorithm for exact real-number integration.
    In this talk I will explain the basic idea, and report on my initial experiments in applying it to the integration problem. I would be very interested in feedback from experienced ML buffs on the following questions:
    • Am I right that my language feature could in principle be implemented efficiently?
    • Am I right that there's currently no other way of achieving the same thing in ML (even with continuations)?
    No particular knowledge of game semantics will be assumed.
  • 10th Dec. Andrew Kennedy Guest talk from Persimmon IT
    Extending SML'97 with a type-safe interface to Java
    Persimmon IT has recently released MLJ, a compiler for SML'97 whose aim is to bring to the ML world the features of Java that have helped it come to prominence so quickly: portability, security, and access to quality code libraries. The latter required extensions to Standard ML that facilitate safe and convenient access to existing Java class libraries and the creation of new Java class libraries written in ML. In this talk I will discuss how we went about designing such an extension and our proposals for a more friendly interface in the next version of MLJ.
    Further Information: Revised Java extensions for ML (Available from local computers only.)
  • 26th Nov. Chris Walton
    Type Directed Translation from ML to Java
    In this talk I will outline a translation system from Standard ML to Java. The translation is defined via a mapping between typed intermediate languages. Unlike the MLJ compiler, the translation is performed at a source-code level and the structure of the ML program is entirely retained (i.e. polymorphism is not removed). The talk will focus on the translation of the core-ML language constructs, as the module-level is still a work-in-progress.
  • 19th Nov. Ian Stark
    Concurrency and Communication in MLJ (Part II)
    The MLJ system recently released by Persimmon IT is an ML compiler that produces bytecodes for the Java Virtual Machine. This leads to code that is immensely portable, can be wrapped up in applets for distribution over the web, and allows for close interworking between ML and Java. Perhaps most importantly it also gives the ML programmer immediate access to the ever-growing supply of Java libraries.
    I am presently writing a small library for concurrent programming in MLJ. As a basis Java provides threads and semaphores; on top of this I have implemented typed channels and event combinators for synchronisation.
    In this talk I shall describe something of how the MLJ compiler operates; what concurrency operations I have implemented; how it's done; and examples of them in action. Finally I shall discuss future possibilities, in particular support for distribution and mobility. This would build on the corresponding Java libraries, but adding the traditional ML favourites of strong typing, type inference and polymorphism.
  • 5th Nov. Ian Stark
    Concurrency and Communication in MLJ (Part I)
    An introduction MLJ.
  • 29th Oct. René Vestergaard Guest talk from Heriot-Watt
    Cut Rules and Explicit Substitutions
    In this talk we will be concerned with the Curry-Howard Correspondence (CHC) for a certain style of inference systems for symbolic logics: Logical deduction (alas, a.k.a. sequent calculus); this is in opposition to the traditional presentation of the CHC which relates natural deduction style inference systems to the well-known lambda-calculus.
    We will initially present a short analysis of the nature of the traditional CHC and use the outcome of this to construct lambda-like calculi that CH-correspond to stylised logical deduction systems. We will show how various of such constructed calculi relate very precisely to known explicit-substitution calculi (ESC), e.g., to lambda-xgc, lambda-s, and lambda-t.
    Certain aspects of these relations are truly remarkable and hitherto unexplored, e.g., the close correspondence between propagation of known cut rules and explicit substitution reduction in known ESC, propagation of weakening rules and propagation of index-updating operators in ESC à la de Bruijn, and, finally, dereliction rules and garbage collection.
    Time permitting we will sketch how various known ESC, in fact, are homomorphic images of logical deduction systems and their, so-called, Hauptsaetze.
  • 22nd Oct. Bruce J. McAdam
    Two Workshops and a Conference
    I have had a busy September, so I will now report on

    • Return to the ML-Club Home Page.