When & Where: 12:30pm, Friday, October 6, 2006, Room 200 AKW
Abstract:
Mathematical programs (MPs) are widely used to represent systems that simultaneously exhibit discrete and continuous phenomena. Until now, the formal definition of an MP has been stated in a low-level canonical form, which does not lead to a practical language for expressing them and leaves numerous questions about their implementation unanswered. In this talk, I summarize the first type theoretic treatment of MP. My main focus will be o= n supporting index sets, which allow making statements such as "for all i in set S, x(i) = y(i)". Following Martin-Lof, we provide a dependent type theory allowing rather rich forms for S. Interestingly, the finitary nature of index sets allows us to define the type system semantically, in contrast to the usual syntactic kind. Constructs exist precisely when they have meaning. Our work also shows that the current practice of MP follows a mixture of the constructive and classical traditions. The net result is an elegant MP language with the confidence of a correct implementation.
Biography:
Ashish recently came to Yale for a postdoctoral position in the labs of Mark Gerstein (MB&B) and Michael Stern (Genetics). He has an interdisciplinary background with degrees in Chemical Engineering and a PhD in the area of programming languages under the guidance of Robert Harper at Carnegie Mellon. His long-term goal is to employ formal methods from CS to develop better software for the natural sciences.