Series: Penn State Logic Seminar Date: Tuesday, October 16, 2001 Time: 2:30 - 3:45 PM Place: 306 Boucke Building Speaker: Hemant K. Bhargava, Management Information Systems, Penn State Title: Analysis of Formal Semantics for a Typed Mathematical Modeling Language Abstract: Ascend, a language for modeling and execution of mathematical programming models, is unique in its use of strong typing. Ascend's type system involves type inheritance, type refinement operators, and dynamic type inference. These features are employed during model development, and the Ascend system encodes an operational semantics for these operators. This talk presents an overview of Ascend, and then develops declarative formal semantics for the language, viewing Ascend statements as sentences in a first-order logic. This formulation allows us to analyze certain represenational and computational properties of Ascend. We develop a class of integrity constraints that is sufficient to obtain certain desirable properties. We demonstrate the existence of a unique "most refined type" for each Ascand object, and show that it can be computed in finite steps. We show that when a model statement is added in Ascend (this may change type properties of many other objects), it is consistency-preserving after type propogation as long as integrity constraints are satisfied by the objects mentioned in the sentence. Finally we uncover the motivations for various (arbitrary-seeming) design decisions made by Ascend developers, by showing, for example, that these restrictions are a necessary conditions for the computation of a unique most refined type.