Richard Eisenberg
Ph.D. Candidate
Department of Computer and Information Science
University of Pennsylvania

"Type-Safe and Sound in an Inconsistent World"

Monday, February 8, 3:00 PM
Packard Lab room 466

Abstract:  Software failures are a common occurrence in today's world. Simple coding mistakes cause corporate embarrassment and financial loss, not to mention frustration for users. In an attempt to ameliorate this problem, researchers have developed multiple techniques for software verification. These techniques can prove that a program works as desired, thereby ruling out many of the failures we hear about in the news. This talk will describe one such technique: dependent types. I will describe recent innovations in the design of the Haskell programming language enabling dependent types, and I will show how fancy types can be used to avoid whole classes of errors. Industrial users of Haskell are already using dependent-type techniques to ensure correctness of their programs. A key detail sets Haskell apart from other dependently typed languages: Haskell is inconsistent as a logic, yet remains type-safe. Dependently typed programs in Haskell need no termination proofs, and the language has the ability to run afoul of Girard's paradox. Type safety is retained, however, by keeping type equalities separate from other terms.

Bio:  Richard Eisenberg is a doctoral candidate at the University of Pennsylvania, specializing in programming language research and supported by a Microsoft Research Graduate Fellowship. The goal of his research is to enable working programmers to detect and eliminate bugs at compile time, with a reduced need for runtime testing. He is also hoping that programming language innovation sees its way into the classroom so that compilers can aid newer programmers in improving their craft. Richard is a core developer of the Glasgow Haskell Compiler, having added several major new features to the language and compiler over the past few years. Prior to his doctoral studies, Richard taught high school computer science and math at independent schools in Massachusetts and London, England. He holds a bachelor's degree in physics and a master's degree in computer science from Harvard.

© 2014-2016 Computer Science and Engineering, P.C. Rossin College of Engineering & Applied Science, Lehigh University, Bethlehem PA 18015.