This website contains a list of papers about or closely related to 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
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
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
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.
This page is maintained by
your comments are welcome.