1. تمرین‌ سری دوم از مبحث حساب لاندا: تمرین‌های ۱.۷.۴ و ۱.۷.۵ و ۱.۷.۶ و ۱.۷.۷ از کتاب. موعد تحویل: شنبه ۱۹ اسفند. ابتدای کلاس درس.
  2. نحوه‌ی محاسبه‌ی نمره: ۹ نمره پایان‌ترم (از حساب lambda و منطق شهودگرایی) +  ۱ نمره تمرین (از حساب lambda و منطق شهودگرایی) + ۷ نمره تمرین‌های Coq + سه نمره پروژه Coq
  3. تمرین‌ Basics-A: (تا ۲۳ بهمن) فصل Basics، تا ابتدای Proof By Simplification. فرمت فایلی که می‌فرستید این‌طور باشد: اگر شماره دانشجویی من ۶۱۱۶۷۲۱۸ باشد، برای این سری از تمرین‌ها نام فایلی که می‌فرستم باید این‌گونه باشد: Basics-A-61167218.v
  4. کتاب کمکی درس: Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
  5. کتابِ درس (دوم): http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
  6. کتاب راهنمای مرجع Coq.
  7. کتابِ  درس (نخست): http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
  8. برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
  9. راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
  10. این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که   توسط مجتبی مجتهدی در دانشگاه تهران (ترم بهار ۱۳۹۶) ارائه می‌شود.