×
Hickey, Jason J.

Nuprl-Light: an implementation framework for higher-order logics. (English) Zbl 1430.68411

McCune, William (ed.), Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1249, 395-399 (1997).
For the entire collection see [Zbl 1415.68038].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B16 Higher-order logic
68V20 Formalization of mathematics in connection with theorem provers

Software:

Isabelle; Nuprl; Cambridge LCF; Nuprl-Light
PDF BibTeX XML Cite
\textit{J. J. Hickey}, Lect. Notes Comput. Sci. 1249, 395--399 (1997; Zbl 1430.68411)
Full Text: DOI
  • logo of hbz
  • logo of WorldCat

References:

[1] Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken. The semantics of reflected proof. In Proceedings of the Fifth Conference on Logic in Computer Science, pages 195-197, June 1987.
[2] R.L. Constable et.al. Implementing Mathematics in the NuPRL Proof Development System. Prentice-Hall, 1986.
[3] Timothy G. Griffin. Notational Definition and Top-Down Refinement for Interactive Proof Development Systems. PhD thesis, Cornell University, 1988.
[4] Rober Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1), January 1993. · Zbl 0778.03004
[5] Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st Annual ACM Symposium on Principles of Programming Languages, pages 123-137. ACM, January 1994.
[6] Jason J. Hickey. Formal objects in type theory using very dependent types. In Foundations of Object Oriented Languages 3, 1996. Available electronically through the FOOL 3 home page at Williams College.
[7] Douglas J. Howe. Equality in Lazy Computation Systems. In Fourth Annual Symposium on Logic in Computer Science, pages 198-203. IEEE Computer Society Press, 1989. · Zbl 0716.68065
[8] Lawrence C. Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Cambridge Univ. Press, 1987. · Zbl 0645.68041
[9] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer LNCS 828, 1994. · Zbl 0825.68059
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.