1.  جدول زمانی ارائه‌ی پروژه‌ها و زمان امتحان  (لیست شماره‌ی تمرین‌ها و فصل مربوط به آن را این‌جا ببینید)
  2. تمرین‌های سری هفتم از کتاب دوم: مطالعه‌ی بخش‌ «Equiv»  حل تمرین‌های  «Recommended»
  3. تمرین‌های سری ششم از کتاب دوم: مطالعه‌ی بخش‌ «Imp»   و حل تمرین‌های  «Recommended»
  4. نمرات ارائه‌ها
  5. تمرین‌های سری پنجم از کتاب دوم: مطالعه‌ی بخش‌ «IndProp» و «Maps» و حل تمرین‌های  «Recommended»
  6. تمرین‌های سری چهارم از کتاب دوم: مطالعه‌ی بخش‌های «Tactics» و «Logic» و حل ۶ تمرینِ «Recommended» (هر فصل ۳ تمرینِ Recommended دارد). توجّه: تمرینِ آخر فصلِ «Logic» نمره‌ی اضافه دارد.
  7. تمرین سری سوم از کتاب دوم: مطالعه‌ی بخش «Poly» و حل تمرین‌های آن به‌جز تمرین آخر. موعد تحویل: یکشنبه ۳ اردیبهشت، پیش از کلاس درس.
  8. تمرین سری ۲ از کتاب دوم: مطالعه‌ی بخش‌های «Induction»  و «Lists»   و حل تمرین‌های این دو فصل به‌علاوه‌ی تمرین‌های اضافه‌ی باقی‌مانده از دو فصل نخست کتاب و ارسال آن‌ها از طریق ای-میل. موعد تحویل: قبل از یکشنبه ۲۷ فروردین ساعت ۱۰ صبح.
  9. تمرین سری۱ از کتاب دوم: مطالعه‌ی بخش‌های «Preface» و «Basics» و حل تمرین‌های این دو فصل (به جز بخش‌های اختیاری انتهای فصل دوم) و ارسال آن‌ها از طریق ای-میل. موعد تحویل: قبل از یکشنبه ۲۰فروردین ساعت ۱۰ صبح.
  10. کتابِ درس (دوم): http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
  11. تمرین سری سوم:  مطالعه‌ی فصل سوم (Introducing Inductive Types) از کتاب نخست درس تا تاریخ سه‌شنبه ۱۵ فروردین.
  12. کتاب راهنمای مرجع Coq.
  13. کتابِ  درس (نخست): Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
  14. برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
  15. راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
  16. این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که   توسط مجتبی مجتهدی در دانشگاه تهران (ترم بهار ۱۳۹۶) ارائه می‌شود.
  1. نمرات نهایی محاسبه شده در درس مبتنی بر ارائه‌ی نهایی pdf icon small
  2. نمرات پروژه‌های تحویل داده شده در طول ترم (Coq): pdf icon small
  3. نمرات تمرین‌های تحویل داده شده در طول ترم (Lambda Calculus & Intuitionistic Logic): pdf icon small
  4. نمرات تمرین‌های تحویل داده شده در طول ترم (Coq): pdf icon small
  5. نمرات امتحان پایان‌ترم  pdf icon small
  6. سؤالات امتحان پایان‌ترم  pdf icon small
  7. تمرین‌های فصل Imp کتاب: تمرین‌های ۳ستاره (۹ تمرین)
  8. تمرین‌ سری دوم از مبحث حساب لاندا: تمرین‌های ۱.۷.۴ و ۱.۷.۵ و ۱.۷.۶ و ۱.۷.۷ از کتاب. موعد تحویل: شنبه ۱۹ اسفند. ابتدای کلاس درس.
  9. نحوه‌ی محاسبه‌ی نمره: ۹ نمره پایان‌ترم (از حساب lambda و منطق شهودگرایی) +  ۱ نمره تمرین (از حساب lambda و منطق شهودگرایی) + ۷ نمره تمرین‌های Coq + سه نمره پروژه Coq
  10. تمرین‌ Basics-A: (تا ۲۳ بهمن) فصل Basics، تا ابتدای Proof By Simplification. فرمت فایلی که می‌فرستید این‌طور باشد: اگر شماره دانشجویی من ۶۱۱۶۷۲۱۸ باشد، برای این سری از تمرین‌ها نام فایلی که می‌فرستم باید این‌گونه باشد: Basics-A-61167218.v
  11. کتاب کمکی درس: Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
  12. کتابِ درس (دوم): http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
  13. کتاب راهنمای مرجع Coq.
  14. کتابِ  درس (نخست): http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
  15. برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
  16. راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
  17. این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که   توسط مجتبی مجتهدی در دانشگاه تهران (ترم بهار ۱۳۹۶) ارائه می‌شود.



  1. توجّه مهم: موعد تحویل پروژه‌ها روز سه‌شنبه ۲۵ تیر، در کلاس ۱۰۹ ساعت ۱۴ می‌باشد. حضور دانشجویایان برای تحویل پروژه الزامی است.
  2. پروژه‌ی درس(۲۵ تیر): انجام ۳ تمرین ۵ستاره یا ۶ تمرین ۴ ستاره یا پیاده‌سازی پروژه‌ی انتخاب شده.
  3. تمرین ۱۰ (۲۵ تیر): تمرین‌های (hoare_asgn_example4)(hoare_asgn_fwd)(hoare_havoc) از Hoare.v.
  4. تمرین ۹ (۲۵ تیر): تمرین‌های (IFB_false) (swap_if_branches) (WHILE_true) (assign_aequiv) (fold_constants_com_sound) (inequiv_exercise) از Equiv.v
  5. تمرین ۸ (۲۵ تیر): تمرین‌های (optimize_0plus_b_sound) (bevalR) (pup_to_n) (XtimesYinZ_spec) (loop_never_stops) (no_whiles_eqv) (stack_compiler) از Imp.v.
  6. تمرین ۷ (۱۶ اردیبهشت): تمرین‌  (t_update_permute) از فصل Maps.v و   (plus_one_r') و (byntree_ind)  از فصل IndPrinciples.v
  7. تمرین ۶ (۹ اردیبهشت): تمرین های (double_neg_inf) (contrapositive) (or_distributes_over_and) (dist_not_exists)(All) (combine_odd_even)(All_forallb)(excluded_middle_irrefutable)(not_exists_dist) از فصل Logic.v و تمرین‌های (ev_ev__ev) (R_provability) (reflect_iff) (beq_natP_practice) (nostutter_defn) از فصل IndProp.v
  8. تمرین ۵ (۲۶ فروردین): تمرین‌های silly_ex apply_exercise1 apply_with_exercise plus_n_n_injective beq_nat_true gen_dep_practice combine_split destruct_eqn_practice forall_exists_challenge از فصل Tactics.v
  9. تمرین ۴:‌ (۱۹ فروردین) همه‌ی تمرین‌های  Lists.v و Poly.v
  10. تمرین ۳:‌ (۲۰ اسفند) همه‌ی تمرین‌های  Induvtion.v
  11. تمرین ۲: Basics.v (۱۳ اسفند) andb_true_elim2 zero_nbeq_plus_1 decreasing boolean_functions andb_eq_orb binary
  12. تمرین ۱: Basics.v (۴ اسفند) nandb andb3 factorial blt_nat plus_id_exercise mult_S_1
  13. کتاب کمکی درس: Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
  14.  کتاب درس، نسخه‌ی سازگار با 8.6 Coq
  15. کتابِ درس: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
  16. کتاب راهنمای مرجع Coq.
  17. برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
  18. راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
  19. برای دریافت اخبار درس، ای-میل خود را در فرم سمت چپ صفحه وارد کنید.
  20. این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که که به صورت مشترک با آقای دکتر علیزاده  در دانشگاه تهران (ترم بهار ۱۳۹۸) ارائه می‌شود.