111 Cummington St., Boston, MA 02215 | cs-www.bu.edu
Last updated: July 20, 2010

Modularity Seminar

Organization Schedule Themes
  • Organization
    • Seminar coordinators: Assaf Kfoury, Franklyn Turbak, Hongwei Xi
    • Meeting time: Spring 2002 -- Monday, from 3:00 to 5:00 pm.
    • Meeting place:Room B32, Cummington Street 111, Boston University.

  • Schedule
    • 02/04/2002
      First-class Modules for Haskell, presented by Assaf Kfoury.
      paper: pdf, ps.   Seminar Slides, Agenda.
    • 02/11/2002
      First-class Modules for Haskell (Cont.), presented by Assaf Kfoury and Gang Chen.
      Seminar Slides.
    • 02/18/2002
      Vacation,Presidents' Day.
    • 02/25/2002
      Branching types,presented by Christian HaackDetails; Slides: pdf, ps.
    • 03/04/2002
      Vacation,Spring Break.
    • 03/11/2002
      No seminar.
    • 03/18/2002
      No seminar.
    • 03/25/2002
      Guarded Recursive Datatype Constructors , presented by Gang Chen. Slides: ps.
    • 04/01/2002
      Toward Better Language Support for Resource-Aware Programming (RAP), presented by Walid Taha from Yale University. Slides: pdf.
    • 04/08/2002
      No seminar.
    • 04/15/2002
      Vacation,Patriots' Day.
    • 04/22/2002
      STATIC MEMORY MANAGEMENT SYSTEM AND ITS MACHINE VERIFICATION, presented by
      IAN C. WESTMACOTT.
    • 04/29/2002
      No seminar.
    • 05/06/2002
      Coming Soon!
    • 05/13/2002
      Coming Soon!

  • Themes:
    • Enhancing the Technology of Intersection Types
      READING:
        Primary:
      • Kfoury, Wells. In POPL 1999. Introduces expansion variables and System I.
      • Wells, Haack. In ESOP 2002. Introduces branching types and lambda-B.
      • Amtoft, Turbak. In ESOP 2000.
      • Wells, Dimock, Muller, Turbak. In JFP 2002. Introduces lambda-CIL.
        Secondary:
      • Van Bakel. Ph.D. thesis.
      • Barbanera, Dezani, de'Liguoro. In MSCS.

      RESEARCH:

      • Extend expansion variable technology to work with intersection types that have properties similar to associativity, commutativity, and idempotence of the intersection type constructor. The resulting system should have subject reduction, unlike System I.
      • Develop a system integrating the features of expansion variables and branching types.
      • Extend the above-mentioned technology to work with real-world programming language features like records, variants, and mutually recursive definitions.
    • Module Calculi
      READING:
      • Cardelli, POPL 1997
      • Shao, Typed Cross-Module Compilation, ICFP 1998
      • Machkasova, Turbak. ESOP 2000.
      • Wells, Vestergaard. ESOP 2000.
      • Fisher, Reppy, Riecke, A Calculus for Compiling and Linking Classes,ESOP 2000
      • Hirschowitz, Leroy. ESOP 2002
      • Ancona, Zucca. A Calculus of Module Systems, JFP.

      RESEARCH:

      • Dealing with assignments and other imperative operations. Partial progress by Hirschowitz & Leroy and Hirschowitz & Wells.
      • Type systems for modules. In particular, mediating between intersection/union types and universal/existential types.
      • Link-time optimization and cross-module transformations: extending calculi to formally describe more transformations,justifying correctness.
      • Abstracting over the base calculus.
      • Issues of call-by-value/name/need in the context of module calculi.
      • Exploring relationships between modules and object-oriented programming.
    • XML-Technology-Based Standards for Manipulating Computer Programs
      READING:
      • Forest/Hedge Automata Theory (very relevant for XML type checking)
      • Functional programming + recursive data types + XML:
        1. Static types for dynamic documents (Mark Shields' thesis)
        2. Scheme and XML
        3. XMLambda
        4. Haskell and XML
        5. \dl-calculus and DL (Santiago Pericas' thesis).Pointers to the preceding can be found at http://types.bu.edu/xml
      • RelaxNG: next generation schema language for XML
      • Stuff on XML Schema, XDuce, RELAX NG. http://www.xml.com/lpt/a/2001/12/12/schemacompare.html
      • Burckhardt. M.A. Thesis 2000.
      • The Cornell Synthesizer Generator and Its Successors (tree-based syntax editors). Web link?
      • Stuff on incremental analysis/compilation during editing. Web link?

      RESEARCH:

      • Standardizing XML vocabularies/dialects for representing programs in particular languages.
      • Developing cross-programming-language standards for representing common features.
      • Developing technology for principal-typing-based incremental analysis/compilation during editing. (Technically, this has nothing to do with XML specifically, but only with trees.However, doing this to full advantage depends on standards for representing/communicating trees.)
      • XML Transformations: transformation languages, static typing, regular automata vs. hedge/tree automata.
    • Type Systems for Modules Without Dependent Types

    Remarks: Descriptions for the first 3 of these topics are collectively written by Joe, Lyn, Elena, Santiago and Assaf. These topics are currently pursued by several of them. The purpose is to increase interaction and the possibility of finding collaborators (among faculty, post-docs and students).