References for Belle
Main
F.A.Q.
References
Contact
Here is some of the literature used or browsed during the design and implementation of Belle.
LCF Implementations
Harrison, John and Konrad Slind.
A Reference Version of HOL
.
Harrison, John.
HOL Done Right
.
Paulson, Lawrence C.
The Foundation of a Generic Theorem Prover
.
Paulson, Lawrence C.
Isabelle: The Next 700 Theorem Provers
.
Paulson, Lawrence C.
Designing a Theorem Prover
.
General Programming
Aho, Alfred V., Ravi Sethi, and Jeffrey D. Ullman.
Compilers: Principles, Techniques, and Tools
.
Chitil, Olaf.
Pretty Printing with Lazy Dequeues
.
Hughes, John.
The Design of a Pretty-printing Library
.
Okasaki, Chris.
Purely Functional Data Structures
.
Miscellaneous
Baader, Franz and Tobias Nipkow.
Term Rewriting and All That
.
Huet, Gerard. A Unification Algorithm for Typed λ-Calculus.
Hurd, Joe.
Predicate Subtyping with Predicate Sets
.
Melham, Thomas F.
The HOL Logic Extended with Quantification over Type Variables
.
Nipkow, Tobias.
Order-Sorted Polymorphism in Isabelle
.
Nipkow, Tobias and Christian Prehofer.
Type Reconstruction for Type Classes
.
Wadler, Philip and Stephen Blott.
How to make
ad-hoc
polymorphism less
ad hoc
.
Wenzel, Markus.
Type Classes and Overloading in Higher-Order Logic
.