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


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.