Innovations in computational type theory using Nuprl

For twenty years the Nuprl ("new pearl") system has been used to develop software systems and formal theories of computational mathematics. It has also been used to explore and implement computational type theory (CTT)

• Type: Journal
• Year: 2006
• Where: JAPLL
• Authors: Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, E. Moran
• Keywords: JAPLL 2006, Nuprl, Theory, Type Theory