@inproceedings{ATS-frocos05,
author = "Sa Cui and Kevin Donnelly and Hongwei Xi",
title = {{ATS: A Language That Combines Programming with Theorem Proving}},
booktitle = "Proceedings of the 5th International Workshop on Frontiers of Combining Systems",
year = 2005,
month = "September",
address = "Vienna, Austria",
pages = "310-320",
abstract = {{
ATS is a language with a highly expressive type system that supports a
restricted form of dependent types in which programs are not allowed to
appear in type expressions.  The language is separated into two components:
a proof language in which (inductive) proofs can be encoded as (total
recursive) functions that are erased before execution, and a programming
language for constructing programs to be evaluated.  This separation
enables a paradigm that combines programming with theorem proving.  In this
paper, we illustrate by example how this programming paradigm is supported
in ATS.
}}
}