M. Bezem, T. Coquand, и S. Huber. 19th International Conference on Types for Proofs and Programs (TYPES 2013), том 26 из Leibniz International Proceedings in Informatics (LIPIcs), стр. 107--128. Dagstuhl, Germany, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, (2014)