Taclets and the KeY prover
The work
| Authors | Martin Giese |
|---|---|
| Editors | |
| Type | article |
| Year | 2004 |
| Citekey | giese2004taclets |
Where it appeared
| Published in | Electronic Notes in Theoretical Computer Science |
|---|---|
| Volume | 103 |
| Pages | 67--79 |
Identifiers
| DOI | 10.1016/j.entcs.2004.09.014 |
|---|
Related
| Distinct from | beckert2004taclets |
|---|
Abstract
We give a short overview of the KeY prover – which is the proof system belonging to the KeY tool [1] – from a user interface perspective. In particular, we explain the concept of taclets, which are the basic building blocks for proofs in the KeY prover.
A copy is held
pdf, 207.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-14 11:32 UTC |
Filed under
Cite it as
@article{giese2004taclets,
title = {Taclets and the KeY prover},
author = {Martin Giese},
year = {2004},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {103},
pages = {67--79},
doi = {10.1016/j.entcs.2004.09.014},
}
This record lives at https://refs.drheap.org/giese2004taclets/ and will keep doing so.