ATS/LF: A type system for constructing proofs as total functional programs. (English) Zbl 1226.68026
Benzmüller, Christoph (ed.) et al., Reasoning in simple type theory. Festschrift in honor of Peter B. Andrews on his 70th birthday. London: College Publications (ISBN 978-1-904987-70-3/pbk). Studies in Logic (London) 17. Mathematical Logic and Foundations, 443-467 (2008).
From the introduction: We have designed and implemented ATS, a programming language with its type system rooted in \(\mathcal {ATS}\) (see [the author, “Applied type system”, Lect. Notes Comput. Sci. 3085, 394–408 (2004; Zbl 1100.03518), http://www.cs.bu.edu/~hwxi/academic/drafts/ATS.ps]). The work we report here is primarily motivated by a need for combining programs with proofs in ATS.
For the entire collection see [Zbl 1196.03002].
For the entire collection see [Zbl 1196.03002].
MSC:
| 68N18 | Functional programming and lambda calculus |
| 03B70 | Logic in computer science |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
