### SPAM Talk: A Type System for Mathematical Programming

**Speaker:**
Ashish Agarwal,
Yale University
**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.