ATS: a Language to Support Practical Programming with Theorem Proving

Trustees Of Boston University, Boston

Investigators

Abstract

Proposal Number: CCF-0702665 TITLE: ATS: A Language to Support Practical Programming with Theorem Proving PI: Hongwei Xi The immense complexity in software design and implementation is evident. In this day and age, software design is often expressed in forms of varying degree of formalism, ranging from verbal discussions to plain text descriptions to UML diagrams to specifications in languages like Z. Also, there is often an enormous gap between the design of a system and its actual implementation, making it exceedingly difficult to construct software meeting its specification. However, the very ability to construct software meeting its specification is crucial to (highly) dependable computing, and there seem to be no other shortcuts. The proposed research focuses on the design and implementation of a full-fledged programming language ATS with a type system rooted in the recently developed framework Applied Type System. In ATS, (certain) specifications in software design can be formally captured in terms of types and then be verified through type-checking. In stark contrast to pure theorem proving systems where programs are extracted from proofs, ATS is an effective programming language that contains a pure theorem-proving subsystem to support programming with theorem proving. The effectiveness of ATS is to be evaluated in the construction of real and complex systems.