Abstract (Summary)
The notion of dependent types has been around for more than three decades, but a major complication resulting from introducing such a type discipline is that pure type inference for the enriched system is no longer possible. However, in the late nineties, a restricted form of dependent types was introduced in practical programming to capture more program properties through types and thereby detect more program errors at compile-time than effected by the strong type discipline in Standard ML or Java. Xanadu, a dependently typed imperative programming language, was the result of enriching the type system of imperative programming paradigm with a restricted form of dependent types. For the effective compilation of Xanadu program, it is crucial to successfully solve the linear constraints generated during its type-checking. This study is focussed on solving and verifying the linear integer constraints generated during the type-checking of Xanadu program. We present a two-tier constraint solver, based on the well-known linear programming algorithm, the Simplex method. The first tier uses the two-phase Simplex method to find a rational solution for a given set of constraints. If no rational solution exists, then no integer solution could be found. However, if a rational solution exists, the second tier uses branch and bound method, an integer programming algorithm, to seek an integer solution. As a significant application, we also study the use of our solver in eliminating the need for array bounds checking at runtime. The solver also generates a data structure, which we designate as history matrix, that records the operations of the Simplex algorithm. We claim that verifying the constraints using this data structure is faster than verifying them through the solver. Several constraints, gathered from the type-checking of Xanadu programs are solved and verified using the history matrix. The results presented, validate our claim. Moreover, we regard this matrix as a representation of a proof, which along with the compiled code would form an effort aimed towards producing a certifying code or a proof carrying code for Xanadu.
Bibliographical Information:


School:University of Cincinnati

School Location:USA - Ohio

Source Type:Master's Thesis

Keywords:simplex algorithm verification linear constraints xanadu dependent types


Date of Publication:01/01/2003

© 2009 All Rights Reserved.