Papers about ATS


This website contains a list of papers about or closely related to ATS.

  • Dependent Types in Practical Programming (pdf) (ps) (thesis.pdf) (thesis.ps)

  • Dependent Types for Program Termination Verification (pdf) (ps)

  • Dependently Typed Pattern Matching (pdf) (ps)
    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.

  • Dependently Typed Data Structures (pdf) (ps)
    The paper contains several data structures (e.g., braun trees, red-black trees, binomial heaps) implemented in Dependent ML, the predecessor of ATS.

  • Imperative Programming with Dependent Types (pdf) (ps)
    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 to supporting imperative programming with dependent types in ATS.

  • Guarded Recursive Datatype Constructors (pdf) (ps)

  • Applied Type System (pdf) (ps)

  • Combining Programming with Theorem Proving (pdf) (ps)

  • Safe Programming with Pointers through Stateful Views (pdf) (ps)

  • ATS/LF: a type system for constructing proofs as total functional programs (pdf) (ps)

  • A Formalization of Strong Normalization for Simply Typed Lambda-Calculus and System F (pdf) (ps)


  • This page is maintained by Hongwei Xi. As always, your comments are welcome.