ATS: A Language That Combines Programming with Theorem Proving

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.

• Type: Conference
• Year: 2005
• Where: FROCOS
• Authors: Sa Cui, Kevin Donnelly, Hongwei Xi
• Keywords: Dependent Types, Expressive Type, FROCOS 2005, Restricted Form