Taclets: A New Paradigm for Constructing Interactive Theorem Provers

The work

AuthorsBernhard Beckert; Martin Giese; Elmar Habermalz; Reiner Hähnle; Andreas Roth; Steffen Schlager
Editors
Typearticle
Year2004
Citekeybeckert2004taclets

Where it appeared

Published inRACSAM
Volume98
Issue1
Pages17--53

Related

Distinct fromgiese2004taclets Two 2004 papers on taclets, KeY's rule-description mechanism, with overlapping authorship and different scope: 'Taclets: A New Paradigm for Constructing Interactive Theorem Provers' states the idea generally, and 'Taclets and the KeY prover' treats its use in the prover itself. Neither reprints or supersedes the other and they were not published together, but a reader who finds one is very likely to want the other, and nothing else in the corpus said so.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-07 23:38 UTC

Cite it as

@article{beckert2004taclets,
  title        = {Taclets: A New Paradigm for Constructing Interactive Theorem Provers},
  author       = {Bernhard Beckert and Martin Giese and Elmar Habermalz and Reiner Hähnle and Andreas Roth and Steffen Schlager},
  year         = {2004},
  journal      = {RACSAM},
  volume       = {98},
  number       = {1},
  pages        = {17--53},
}

This record lives at https://refs.drheap.org/beckert2004taclets/ and will keep doing so.