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).