TY - RPRT TI - Constructing Recursion Operators in Intuitionistic Type Theory AU - Lawrence C. Paulson PY - 2000 UR - https://arxiv.org/abs/cs/9301102 ID - cs/9301102 ER -