I plan to incorporate next semester an introduction to TLA (and
temporal logic) into a graduate introductory course on formal logic
and program verification.
If anyone has any ideas, material, pointers, or experience to share, that would be tremendously helpful and greatly appreciated.
Thanks much in advance and best wishes - Daniel
Professor of computer science
and adjunct professor of mathematics
Indiana University Bloomington