Citations

• Aitken, William and Robert L. Constable. Reflecting on Nuprl Lessons 1-4, Cornell University, Computer Science Dept., Ithaca, NY, 1992.
  
  
• Aitken, William and Robert L. Constable. An Inductive Definition of Evaluation in Nuprl, CS 611 Notes, Cornell University, 1993.
  
  
• Allen, Stuart F.,, Robert L.~Constable, Douglas J.~Howe and William Aitken. The Semantics of Reflected Proof, Proceedings of the Fifth Symposium on Logic in Computer Science, IEEE, 1990, pages 95-197, June, year?
  
  
• U. Berger and H. Schwichtenberg, eds. Formalizing Decidability Theorems about Automata, Series F: Computer and Systems Sciences, NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 29-August 6, 1997, Springer, 1998.
  
  
• need Davis thesis
  
  
• Glynn Morrill, Type-Logical Grammar, 1994
  
  
• Pereira and Warren, "Parsing as deduction," 1983;
  
  
• Pereira, "Semantic interpretation as higher-order deduction," 1991.
  
  
• Ranta book
  
  
• Wang, H., Toward Mechanical Mathematics, IBM Journal of Research and Development, 1960, pages 2-22.