@incollection{ATSLF,
author = "Hongwei Xi",
booktitle = {Festschrift in Honour of {Peter B. Andrews} on his 70th Birthday},
title = {{ATS/LF: a type system for constructing proofs as total functional programs}},
editor = {Christoph Benzm{\"u}ller and Chad Brown and J{\"o}rg Siekmann},
publisher = {IFCoLog},
series = {Studies in Logic and the Foundations of Mathematics},
month = {December},
year = 2008,
}