Software Foundations
- Details
- Hits: 1568
- جدول زمانی ارائه‌ی پروژه‌ها و زمان امتحان (لیست شماره‌ی تمرین‌ها و فصل مربوط به آن را این‌جا ببینید)
- تمرین‌های سری هفتم از کتاب دوم: مطالعه‌ی بخش «Equiv» حل تمرین‌های «Recommended»
- تمرین‌های سری ششم از کتاب دوم: مطالعه‌ی بخش «Imp» و حل تمرین‌های «Recommended»
- نمرات ارائه‌ها
- تمرین‌های سری پنجم از کتاب دوم: مطالعه‌ی بخش «IndProp» و «Maps» و حل تمرین‌های «Recommended»
- تمرین‌های سری چهارم از کتاب دوم: مطالعه‌ی بخش‌های «Tactics» و «Logic» و حل ۶ تمرینِ «Recommended» (هر فصل ۳ تمرینِ Recommended دارد). توجّه: تمرینِ آخر فصلِ «Logic» نمره‌ی اضافه دارد.
- تمرین سری سوم از کتاب دوم: مطالعه‌ی بخش «Poly» و حل تمرین‌های آن به‌جز تمرین آخر. موعد تحویل: یکشنبه ۳ اردیبهشت، پیش از کلاس درس.
- تمرین سری ۲ از کتاب دوم: مطالعه‌ی بخش‌های «Induction» و «Lists» و حل تمرین‌های این دو فصل به‌علاوه‌ی تمرین‌های اضافه‌ی باقی‌مانده از دو فصل نخست کتاب و ارسال آن‌ها از طریق ای-میل. موعد تحویل: قبل از یکشنبه ۲۷ فروردین ساعت ۱۰ صبح.
- تمرین سری۱ از کتاب دوم: مطالعه‌ی بخش‌های «Preface» و «Basics» و حل تمرین‌های این دو فصل (به جز بخش‌های اختیاری انتهای فصل دوم) و ارسال آن‌ها از طریق ای-میل. موعد تحویل: قبل از یکشنبه ۲۰فروردین ساعت ۱۰ صبح.
- کتابِ درس (دوم): http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
- تمرین سری سوم: مطالعه‌ی فصل سوم (Introducing Inductive Types) از کتاب نخست درس تا تاریخ سه‌شنبه ۱۵ فروردین.
- کتاب راهنمای مرجع Coq.
- کتابِ درس (نخست): Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
- برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
- راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
- این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که توسط مجتبی مجتهدی در دانشگاه تهران (ترم بهار ۱۳۹۶) ارائه می‌شود.
- Details
- Hits: 1609
- نمرات نهایی محاسبه شده در درس مبتنی بر ارائه‌ی نهایی
- نمرات پروژه‌های تحویل داده شده در طول ترم (Coq):
- نمرات تمرین‌های تحویل داده شده در طول ترم (Lambda Calculus & Intuitionistic Logic):
- نمرات تمرین‌های تحویل داده شده در طول ترم (Coq):
- نمرات امتحان پایان‌ترم
- سؤالات امتحان پایان‌ترم
- تمرین‌های فصل Imp کتاب: تمرین‌های ۳ستاره (۹ تمرین)
- تمرین سری دوم از مبحث حساب لاندا: تمرین‌های ۱.۷.۴ و ۱.۷.۵ و ۱.۷.۶ و ۱.۷.۷ از کتاب. موعد تحویل: شنبه ۱۹ اسفند. ابتدای کلاس درس.
- نحوه‌ی محاسبه‌ی نمره: ۹ نمره پایان‌ترم (از حساب lambda و منطق شهودگرایی) + ۱ نمره تمرین (از حساب lambda و منطق شهودگرایی) + ۷ نمره تمرین‌های Coq + سه نمره پروژه Coq
- تمرین Basics-A: (تا ۲۳ بهمن) فصل Basics، تا ابتدای Proof By Simplification. فرمت فایلی که می‌فرستید این‌طور باشد: اگر شماره دانشجویی من ۶۱۱۶۷۲۱۸ باشد، برای این سری از تمرین‌ها نام فایلی که می‌فرستم باید این‌گونه باشد: Basics-A-61167218.v
- کتاب کمکی درس: Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
- کتابِ درس (دوم): http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
- کتاب راهنمای مرجع Coq.
- کتابِ درس (نخست): http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
- راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
- این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که توسط مجتبی مجتهدی در دانشگاه تهران (ترم بهار ۱۳۹۶) ارائه می‌شود.
- Details
- Hits: 1657
- توجّه مهم: موعد تحویل پروژه‌ها روز سه‌شنبه ۲۵ تیر، در کلاس ۱۰۹ ساعت ۱۴ می‌باشد. حضور دانشجویایان برای تحویل پروژه الزامی است.
- پروژه‌ی درس(۲۵ تیر): انجام ۳ تمرین ۵ستاره یا ۶ تمرین ۴ ستاره یا پیاده‌سازی پروژه‌ی انتخاب شده.
- تمرین ۱۰ (۲۵ تیر): تمرین‌های (hoare_asgn_example4)(hoare_asgn_fwd)(hoare_havoc) از Hoare.v.
- تمرین ۹ (۲۵ تیر): تمرین‌های (IFB_false) (swap_if_branches) (WHILE_true) (assign_aequiv) (fold_constants_com_sound) (inequiv_exercise) از Equiv.v
- تمرین ۸ (۲۵ تیر): تمرین‌های (optimize_0plus_b_sound) (bevalR) (pup_to_n) (XtimesYinZ_spec) (loop_never_stops) (no_whiles_eqv) (stack_compiler) از Imp.v.
- تمرین ۷ (۱۶ اردیبهشت): تمرین (t_update_permute) از فصل Maps.v و (plus_one_r') و (byntree_ind) از فصل IndPrinciples.v
- تمرین ۶ (۹ اردیبهشت): تمرین های (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
- تمرین ۵ (۲۶ فروردین): تمرین‌های 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
- تمرین ۴: (۱۹ فروردین) همه‌ی تمرین‌های Lists.v و Poly.v
- تمرین ۳: (۲۰ اسفند) همه‌ی تمرین‌های Induvtion.v
- تمرین ۲: Basics.v (۱۳ اسفند) andb_true_elim2 zero_nbeq_plus_1 decreasing boolean_functions andb_eq_orb binary
- تمرین ۱: Basics.v (۴ اسفند) nandb andb3 factorial blt_nat plus_id_exercise mult_S_1
- کتاب کمکی درس: Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
- کتاب درس، نسخه‌ی سازگار با 8.6 Coq
- کتابِ درس: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
- کتاب راهنمای مرجع Coq.
- برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
- راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
- برای دریافت اخبار درس، ای-میل خود را در فرم سمت چپ صفحه وارد کنید.
- این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که که به صورت مشترک با آقای دکتر علیزاده در دانشگاه تهران (ترم بهار ۱۳۹۸) ارائه می‌شود.
- Details
- Hits: 1081
- کتاب کمکی درس: Adam Chlipala , Certified Programming with Dependent Types, a pragmatic introduction to the Coq Proof Assistant, MIT press. نسخه‌ی آنلاین (html) از کتاب درس. نسخه‌ی pdf از درفت همان کتاب.
- کتاب درس، نسخه‌ی سازگار با 8.6 Coq
- کتابِ درس: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
- کتاب راهنمای مرجع Coq.
- برای اجرای دستورات Coq تحت وب، می‌توانید به این پیوند مراجعه کنید.
- راهنمای نصب Coq: در سیستم‌عامل‌های Linux، Windows و Mac OSX.
- کلاس‌های درس از طریق این پیوند اسکایپی و در روزهای یکشنبه و سه‌شنبه ساعت ۲ تا ۴ عصر برگزار می‌شود.
- گروه تلگرام: @ut1400lp
- این‌جا صفحه‌ی اختصاصی درس منطق و الگوریتم است که که به صورت مشترک با آقای دکتر علیزاده در دانشگاه تهران (ترم بهار ۱۳۹۸) ارائه می‌شود.
