Stateless HOL
We present a version of the HOL Light system that supports undoing definitions in such a way that this does not compromise the soundness of the logic. In our system the code that keeps track of the constants that have been defined thus far has been moved out of the kernel. This means that the kernel...
Main Author: | |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2011-03-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1103.3322v1 |