Importing mathematics from HOL into Nuprl
Author:
- 1 January 1996
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 267-281
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- The Definition of Standard ML1997
- PVS: Combining specification, proof checking, and model checking1996
- Semantic foundations for embedding HOL in NuprlLecture Notes in Computer Science, 1996
- Exploring abstract algebra in constructive type theory1994
- The HOL logic extended with quantification over type variablesFormal Methods in System Design, 1993
- Introducing well-founded function definitions in HOL1993
- Constructive Mathematics and Computer Programming1982
- Edinburgh LCF1979