Fellow Haskellers, I am very pleased to announce that I recently completed the degree requirements for my master's. As a part of those requirements, I undertook research that may be of interest to those of you subscribed to this list. My research involved designing and implementing a type verification algorithm for Yhc Haskell bytecode. The final report detailing this research may found at the Tufts CS Department technical reports page [1]. The abstract for the report follows this message. In addition to the report, I have made available the source code for my proof-of-concept implementation, which consists of a simple bytecode compiler and verifier. The source code may be found at the project page for this research [2]. If you have questions or comments please either email me directly or take discussion to the haskell-cafe or yhc mailing lists. Thanks, Rob Dockins [1] http://www.cs.tufts.edu/tr/techreps/TR-2007-2 [2] http://www.eecs.tufts.edu/~rdocki01/masters.html Abstract: In this paper we present a method for verifying Yhc bytecode, an intermediate form of Haskell suitable for mobile code applications. We examine the issues involved with verifying Yhc bytecode programs and we present a proof-of-concept bytecode compiler and verifier. Verification is a static analysis which ensures that a bytecode program is type-safe. The ability to check type-safety is important for mobile code situations where untrusted code may be executed. Type-safety subsumes the critical memory-safety property and excludes important classes of exploitable bugs, such as buffer overflows. Haskell's rich type system also allows programmers to build effective, static security policies and enforce them using the type checker. Verification allows us to be confident the constraints of our security policy are enforced.