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...
Na minha lista:
| Hovedforfatter: | |
|---|---|
| Format: | Artigo |
| Sprog: | Inglês |
| Udgivet: |
Open Publishing Association
2011-03-01
|
| Serier: | Electronic Proceedings in Theoretical Computer Science |
| Online adgang: | http://arxiv.org/pdf/1103.3322v1 |
| Tags: |
Ingen Tags, Vær først til at tagge denne postø!
|