!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
                                       
                   B O S T O N   U N I V E R S I T Y
                                       
                      Computer Science Department
                                       
                          C O L L O Q U I U M

                 Dependent Types in Practical Programming

                              Hongwei Xi

                        University of Cincinnati

                            Monday, March 19
			       11:00 am
                       (Coffee served at 10:45PM)

                         Seminar Room / MCS 135

  We propose to enrich practical programming with a type discipline
  based on dependent types that allows for specification and inference
  of significantly more precise information on programs than those
  enforced in programming languages such as Standard ML (SML) and
  Java.  The primary motivation for developing such a type discipline
  is to enable the programmer to express more program properties with
  types and then enforce these properties through type-checking, thus
  facilitating the detection of more program errors at
  compile-time. We are also interested in studying the use of
  dependent types in certified compilation. In particular, we intend
  to build a compiler that can translate program properties captured
  at source level into corresponding ones at target level.
  
  In this talk, we demonstrate the use of a restricted form dependent
  types in both functional and imperative programming, capturing
  interesting program properties such as memory safety and termination.
  We also mention various key decisions adopted in our language design
  and some potential use of dependent types in producing proof
  certificates for proof carrying code.
  
Host: Ibrahim Matta
-------------------------------------------------------------------------------
For colloquium info, including directions, see http://cs-www.bu.edu/colloquium
-------------------------------------------------------------------------------