I am a mathematics professor ^{*}. I was approached recently by one of our talented computer-science undergraduates at the university where I work, who is in her senior year and interested in taking a reading course in the applications of mathematical logic to computer science.

This undergraduate recently completed a summer project with the author of Twelf, formalising the ‘simplification’ SASyLF, and I get the impression that her interest is much more in the sorts of logic that arise in computer-assisted (mathematical) theorem proving than in the logic of programming *per se*—that is, I think that she's not particularly interested in temporal logic and other such proving-programs-correct stuff. She specifically mentioned wanting to understand the SLDNF logic behind Prolog, and I feel qualified to start there, but don't really know where to go next. I guess that I want to dig deeper into HM type inference (although she's already studied TAPL on her own, I believe), the calculus of inductive constructions, and that sort of thing—but these are mostly just (to me) buzzwords that I've picked up, and I'd like to put together some sort of coherent reading course. Suggestions?

^{*} To clarify, I'm mentioning this not to brag, but rather to give an idea of what a stretch this course will be for me. (I'm a representation theorist, not a logician.) Thus, don't hesitate to give references to things that “everybody knows”—almost assuredly, I don't!

## Recent comments

2 days 5 hours ago

3 days 37 min ago

3 days 4 hours ago

3 days 5 hours ago

3 days 6 hours ago

3 days 6 hours ago

3 days 7 hours ago

3 days 7 hours ago

3 days 11 hours ago

3 days 11 hours ago