Papers about ATS

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language L that is completely separate from run-time programs, leading to the DML(L) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions.

The original version of DML is presented here. The paper is an extended abstract of the thesis.

Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic running examples to support the effectiveness of this approach to program termination verification as well as its unobtrusiveness to programming.

In the presence of dependent datatypes, the sequentiality of pattern matching (as is supported in ATS) interacts with type-checking. This, for instance, is clearly explained in the implementation of the function zip1 available here. In this paper, the interaction between sequential pattern matching and type-checking is formally studied, and a means is provided for the programmer to control such interaction.

The paper contains several data structures (e.g., braun trees, red-black trees, binomial heaps) implemented in Dependent ML, the predecessor of ATS. For people interested in using dependent types to capture invariants in data structure, the paper is a good start.

This paper presents a design for supporting dependent types in imperative programming. While this design is simple, it is rather inflexible and does not seem to be able to handle imperative data structures such as (singly or doubly) linked lists and binary trees. Nonetheless, this paper may help the reader understand the current approach, which is general and flexible, to supporting imperative programming with dependent types in ATS.

The paper introduces a notion of guarded recursive (g.r.) datatype constructors, generalizing the notion of recursive datatypes in functional programming languages such as ML and Haskell. Both theoretical and practical issues resulted from this generalization are addressed. On one hand, a type system is designed to formalize the notion of g.r. datatype constructors and its soundness is proven. On the other hand, some significant applications (e.g., implementing objects, implementing staged computation, etc.) of g.r. datatype constructors are given, indicating that g.r. datatype constructors can have far-reaching consequences in programming. The main contribution of the paper lies in the recognition and then the formalization of a programming notion that is of both theoretical interest and practical use.

Applied Type System (ATS) is recently proposed as a framework for designing and formalizing (advanced) type systems in support of practical programming. In ATS, the definition of type equality involves a constraint relation, which may or may not be algorithmically decidable. To support practical programming, we adopted a design in the past that imposes certain restrictions on the syntactic form of constraints so that some effective means can be found for solving constraints automatically. Evidently, this is a rather ad hoc design in its nature. In this paper, we rectify the situation by presenting a fundamentally different design, which we claim to be both novel and practical. Instead of imposing syntactical restrictions on constraints, we provide a means for the programmer to construct proofs that attest to the validity of constraints. In particular, we are to accommodate a programming paradigm that enables the programmer to combine programming with theorem proving. Also we present some concrete examples in support of the practicality of this design.

Proof erasure plays an essential role in the paradigm of programming with theorem proving as is supported in ATS. In this paper, a form of attributive types are introduced that carry an attribute to determine whether expressions assigned such types are eligible for erasure before run-time. A type system to support this form of attributive types is formalized and its soundness is established. In addition, an extension of the developed type system with dependent types is outlined and some examples are presented to illustrate some practical use of attributive types.

The paper gives a brief introduction to using (stateful) views in support of safe programming with pointers (and pointer arithmetic). It is a good start for people interested in programming with theorem-proving in an imperative setting.

This paper outlines the design of ATS/LF, the theorem proving component in ATS (for supporting programming with theorem-proving). In particular, it demonstrates, with interesting examples, an approach to theorem proving that represents proofs as total functions. The paper is especially important for people interested in using ATS/LF as a logical framework to encode deduction systems as well as to reason about their (meta-)properties.

The paper first presents in details the encoding of a proof (based on Tait's notion of reducibility) in ATS showing that the simply-typed lambda-calculus is strongly normalizing. It then encodes in ATS a proof (based on Girard's notion of reducibility candidates) showing that System F is strongly normalizing.