------

Title: To memory safety through proofs

Speaker: Hongwei Xi (Boston University)

Abstract:

The need for direct memory manipulation through pointers is essential in
many applications and especially in those that involve systems
programming. However, it is also commonly understood that the use (or
probably misuse) of pointers is often a rich source for program errors.  In
safe programming languages such as ML and Java, it is completely forbidden
to make explicit use of pointers and memory manipulation is done through
systematic allocation and deallocation. In order to cope with applications
requiring direct memory manipulation, these languages often provide a means
to interface with functions written in unsafe languages such as C. While
this is a workable design, the evident irony of this design is that often
the most difficult part of programming must be done in a highly error-prone
manner with little, if there is any, support of types. This design
certainly goes against the efforts to promote the use of safe languages
such as ML and Java.

Currently, we are in the process of designing and implementing ATS, a
programming language with an advanced type system rooted in a recently
developed framework Applied Type System.  In this talk, we are to
demonstrate that the type system of ATS is capable of guaranteeing the
memory safety of programs that may involve (sophisticated) pointer
manipulation such as pointer arithmetic. In particular, we present an
approach that ascribes ATS types to C library functions so as to facilitate
safe programming with these functions. For the purpose of illustration, we
focus on certain interesting C functions that handle resources such as
files and memory.

------

Bio:

Hongwei Xi is currently an assistant professor in the Computer Science
Department at Boston University. He received his Doctoral degree in Pure
and Applied Logic from Carnegie Mellon University (CMU), PA, 1998.  After
working as a postdoctoral researcher at Oregon Graduate Institute (OGI) of
Science and Technology, he joined the University of Cincinnati in September
1999 and then Boston University in Octorber 2001.

Dr. Xi has performed research in various areas of computer science:
automated theorem proving, rewriting systems, type theory, etc.  In
particular, he is interested in programming language design and
implementation through the use of advance type theory and has done some
pioneering work in making dependent types available for practical
programming. Dr. Xi has published a large body of research papers and is
a recipient of the NSF CAREER Award.

------