If you'd like to read more background material, here are some recommended texts and papers:
- 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
"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.
- "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.