A higher-order implementation of rewriting (Q800739)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A higher-order implementation of rewriting |
scientific article |
Statements
A higher-order implementation of rewriting (English)
0 references
1983
0 references
This paper describes the implementation of rewriting in LCF (the interactive theorem-prover for Scott's logic of computable functions). Because many theorem-proving tools are written in ML (the metalanguage for LCF) an introduction into ML is presented. Further sections contain detailed descriptions of pattern matching primitives, term conversions, formula conversions and rewriting tactics. Good examples and clear style make the paper very readable.
0 references
implementation of rewriting in LCF
0 references
logic of computable functions
0 references
ML
0 references
pattern matching
0 references
term conversions
0 references
formula conversions
0 references
