SCS Undergraduate Thesis Topics

While a lot of research has gone into the study of type-safety, it has been done with simple contrived languages. There has never been a rigorous formal proof of this important property for any real language. Some prior work has gone into providing a definition of Standard ML, but it is known to contain bugs and was done entirely by hand. This could be greatly improved upon by a machine checkable proof of type-safety for Standard ML. Twelf is a formal logic tool designed for this purpose. The Harper-Stone definition of Standard ML has been formalized in Twelf and a proof of type-safety will be given.