|
Modularity Seminar
-
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 Haack.
Details;
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:
-
Static types for dynamic documents (Mark Shields' thesis)
-
Scheme and XML
-
XMLambda
-
Haskell and XML
-
\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).
|