Home Page for CSCI B522 (Programming Language Foundations)

Syllabus

Code

Assignments

Grades

Announcements:

• In addition to the Featherweight Java chapter in Harper's book, please read the same chapter in Pierce's book. Here is an updated version of the chapter.

• Please fill the course evaluation form.

• An interesting web page about some software engineering connections between monads and type classes and modular decomposition of software and design patterns. You might find an idea for a project there.

• Here is an outline of the proof of type safety for extended MinML. (Postscript or PDF)

• Fresh ideas for projects:
  • Extend MinML with subtyping and implement it (See Ch. 16 of Pierce's book).
  • Implement Featherweight Java.

• I need at least a paragraph describing your project as soon as possible. Please send me something even if you've already talked to me about your project. If you want some guidance or ideas in selecting a project then please stop by.

• Here is a link to a book in preparation by Benjamin's Pierce: Type Systems and Programming Languages. The book goes in depth in some of the topics that we have only skimmed and have some new topics that we haven't covered at all. If you haven't selected a project yet, I recommend that you select something from the book.

• I have changed the length and date for the Haskell homework. Please check the homework page.

• I have looked at the type safety proofs for MinML with references and recursive types. Most of the papers tried to do the proof by considering each fragment of the language in isolation. This does not work. I will give a counterexample next lecture. Instead of rushing ahead, I am requesting that each one fixes the proof, and only when you are done with the proof, you can move on to the Haskell homework.

• While you are doing the proof of type safety for MiniML with recursive types and references, can you think of a way to reuse parts of the proof for the simple subset? Explore, as a project, how to reformulate things so that you could reuse parts of the proof.

• Another idea for a project about XML came up in class today (Feb 22, 2001). For a starting point on current research related to XML please look at Benjamin Pierce's home page and follow the links to XDuce in the current projects. One possible project would be to write a good survey of the problems, state of the art, and how type theory and the technology we are learning in class might apply.

• For a thorough (but advanced) explanation of monads and effects, consult the following paper:http://www.disi.unige.it/person/MoggiE/APPSEM00/. Some of the exercises in the paper could form the basis of your final project/paper.

• For next week (of Feb 19), I will finish the chapter on products, sums, and recursive types, and then talk about references. The week after we'll start talking about a really elegant treatment of references using monads.

• Grades are posted.

• I have posted my solution to the ML homework. I have chosen to implement the version of the dynamic semantics that exploits the presence of the type checker by representing all values as int without fear of confusion. The code is accessible from this link.

• Tuesday's (Feb 13) lecture will be about Java security from the context of type safety. There is a lot of information out there. Here are some links: Securing Java, Formalization of the JVM, Java verifier flaw, Java type-safety

• I have added more cases to the file static.ml. The new file is called static2.ml and is in the code directory.

• Idea for project: The proof of type safety for MiniML is simple enough but at the same tedious enough that one might reasonably expect to automate it, or at least verify it mechanically. There are several systems called logical frameworks in which one can formalize such proofs. Find such a system, learn about it, and use it to automatically verify the proof of type safety for MiniML.