Simple types in type theory: Deep and shallow encodings

Published in In the proceedings of International Conference on Theorem Proving in Higher Order Logics, 2007