Gloss and rate a book.
Chris Pressey
10 months ago
| 21 | 21 |
Of these, [**107** have the highest rating](by-rating/Top-rated.md),
|
| 22 | 22 |
[**32** are considered classics](by-rating/Classic.md),
|
| 23 | 23 |
[**59** are considered very interesting](by-rating/Very%20Interesting.md),
|
| 24 | |
while [**69** are yet to be rated](by-rating/Unrated.md).
|
|
24 |
while [**67** are yet to be rated](by-rating/Unrated.md).
|
| 25 | 25 |
|
| 26 | 26 |
<!-- /TOTALS -->
|
| 27 | 27 |
|
| 44 | 44 |
|
| 45 | 45 |
* Certified Programming with Dependent Types ([archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes))
|
| 46 | 46 |
* Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft) ([www.ps.uni-saarland.de](https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf))
|
| 47 | |
|
| 48 | |
### Equational Logic
|
| 49 | |
|
| 50 | |
* Canonical Equational Proofs ([archive.org](https://archive.org/details/canonicalequatio0000bach))
|
| 51 | 47 |
|
| 52 | 48 |
### Formal Language
|
| 53 | 49 |
|
|
| 198 | 194 |
|
| 199 | 195 |
### Type Theory
|
| 200 | 196 |
|
| 201 | |
* Recursive Types ([www.ps.uni-saarland.de](https://www.ps.uni-saarland.de/courses/seminar-ws02/RecursiveTypes.pdf))
|
| 202 | 197 |
* Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega ([web.cs.ucla.edu](https://web.cs.ucla.edu/~palsberg/paper/popl16-full.pdf))
|
| 203 | 198 |
|
| 204 | 199 |
Unrated Repos
|
| 30 | 30 |
|
| 31 | 31 |
### Canonical Equational Proofs
|
| 32 | 32 |
|
| 33 | |
* rating: TODO
|
| 34 | |
|
| 35 | |
Book that came from a PhD thesis, looks like. Slightly intriguing. Haven't been able
|
| 36 | |
to wrap my head around it fully.
|
|
33 |
* rating: 0
|
|
34 |
|
|
35 |
A book that came from a PhD thesis. It's short (105 pages once you exclude the
|
|
36 |
frontmatter and bibliography). It's mostly about completion (Knuth-Bendix
|
|
37 |
completion) really.
|
|
38 |
|
|
39 |
Convergent rewrite systems reduce terms to normal forms. Completion finds
|
|
40 |
a convergent rewrite system from an equational system (when it can). Completion
|
|
41 |
systems can themselves be analyzed as equational inference systems.
|
|
42 |
So basically, they give some rules of inference for Knuth-Bendix completion.
|
|
43 |
(Operational semantics...? Probably not.)
|
|
44 |
|
|
45 |
They keep saying that theorem provers can be viewed as proof transformers or
|
|
46 |
proof normalizers. I don't get this bit yet. I think they mean automated
|
|
47 |
theorem provers. Does Knuth-Bendix completion take an existing equational
|
|
48 |
proof and return a transformed (or normalized) rewrite proof? The input is
|
|
49 |
just a set of equations, not a proof (right?) So, this is difficult to see.
|
|
50 |
|
|
51 |
Anyway, this is an extension of the concept of completion, as introduced by
|
|
52 |
Knuth and Bendix. In Plaisted's book chapter on term rewriting he mentions
|
|
53 |
it as "ordered completion". I'm not hugely interested in completion.
|
| 37 | 54 |
|
| 38 | 55 |
### Equational Logic and Abstract Algebra
|
| 39 | 56 |
|