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...

Full description

Bibliographic Details
Main Author: Freek Wiedijk
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