Print
Hits: 1110



  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. این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که که به صورت مشترک با آقای دکتر علیزاده  در دانشگاه تهران (ترم بهار ۱۳۹۸) ارائه می‌شود.