- Instructor: Amr Sabry

- 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.

sabry@cs.indiana.edu