Types for proofs and programs : International Workshop TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers - Coquand, Thierry (Lecture notes in computer science ;, 2000)