Innovations in computational type theory using Nuprl. - Stuart F. Allen; Mark Bickford; Robert L. Constable; Richard Eaton; Christoph Kreitz; Lori Lorigo; E. Moran (J. Appl. Log., 2006)