Sciweavers

Share
FROCOS
2005
Springer

ATS: A Language That Combines Programming with Theorem Proving

9 years 2 months ago
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.
Sa Cui, Kevin Donnelly, Hongwei Xi
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FROCOS
Authors Sa Cui, Kevin Donnelly, Hongwei Xi
Comments (0)
books