Bibliography

If you'd like to read more background material, here are some recommended texts and papers:

Blog Posts

• Lowering Rust traits to logic
• Unification in Chalk, part 1
• Unification in Chalk, part 2
• Negative reasoning in Chalk
• Query structure in chalk
• Cyclic queries in chalk
• An on-demand SLG solver for chalk

Papers

"A proof procedure for the logic of Hereditary Harrop formulas", by Gopalan Nadathur. This paper covers the basics of universes, environments, and Lambda Prolog-style proof search. Quite readable.

"A new formulation of tabled resolution with delay", by Theresa Swift. This paper gives a kind of abstract treatment of the SLG formulation that is the basis for our on-demand solver.

Books

• "Introduction to Formal Logic", Peter Smith
• "Handbook of Practical Logic and Automated Reasoning", John Harrison
• "Types and Programming Languages", Benjamin C. Pierce
• Programming with Higher-order Logic, by Dale Miller and Gopalan Nadathur, covers the key concepts of Lambda prolog. Although it's a slim little volume, it's the kind of book where you learn something new every time you open it.