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

6 hours 41 min ago

8 hours 54 min ago

10 hours 23 min ago

12 hours 11 min ago

13 hours 30 min ago

19 hours 24 min ago

1 day 11 hours ago

1 day 11 hours ago

1 day 11 hours ago

1 day 12 hours ago