a pessimistic researcher

آقا اینو اومدم برای دوستای pl کارم بفرستم و تشویق شون کنم شرکت کنن که گفتم همینجا بذارمش.
لکچر های خیلی خوبی داره و لکچرر هاش هم خیلی قوین. فاند هم برای ساپورت مالی دارن. این سامر اسکول اکثرا آمریکا برگزار می‌شد و امسال فرصت خوبیه که تو اروپاست. البته اون چندتا دوستم همه شون آمریکان و امیدوارم ویزاشون سینگل نباشه :))

Programming Language Implementation Summer School (PLISS) 2025

Location : Bertinoro, Italy
Deadline : 21Jan

https://pliss.org/2025/index.html

#summerschool #pl

از اصحاب کسی پرسید که Stateless Model Checking چیست؟ و ما برایتان پست‌هایی نوشتیم مثل:
"از زاربروکن تا کایزرسلاترن : Stateless Model Checking"
"Software Verification is Our Quest"
"Software Verification is Our Business"
"Fuzzing for free! Except you, concurrency!"
و حتی این، تا برایتان پندی باشد. باشد که مطالب کانال را دنبال کنید :)

"Beware of bugs in the above code; I have only proved it correct, not tried it."
به نظرم همین طعنه‌ی آقای Donald Knuth میتونه لازم و کافی باشه جهت ساپورت کردن این نکته که روش‌های Formal Verification که Statefull هستند (به قولی semantics-driven) و یا مبتنی بر Static Analysis هستند (به قولی Syntax-driven) اصلا مناسب برنامه‌هایی که با یک real programming language نوشته میشن نیستن. بهترین راه، اجرا کردن برنامه است و روش‌های مبتنی بر اون مثل Stateless Model Checking چرا که اگر باگی در برنامه وجود داشته باشه قطعا در runtime بهش میرسیم. این جمله آخر رو دوبار بخون چون من راجع به testing و fuzzing صحبت نمی‌کنم.

این اپیزود از رادیو دیو رو خیلی سال پیش که اومد داداشم برام فرستاد و گوش دادم منتهی نه گیلکیم خیلی خوب بود اون موقع و نه خیلی تونستم با این کانسپت ارتباط بگیرم. ولی خب هر چی که گذشت بیشتر تونستم باهاش ارتباط بگیرم و دوستش داشته باشم. یادمه دوران ارشد با دوستان دانشگاه قسمت شد و یه سفر رفتیم ولایتمون لشتِ نشاء و من اونجا براشون این اپیزود رو گذاشتم و ترجمه میکردم ترانه‌هاش رو :))) ترجمه‌های عمیقی داره ترانه‌های فولک گیلکی :)) مثلا توی ترانه‌ی "حاج خانمه‌ی" که مرحوم عاشورپور خوندن یه جاش میگه که : در جوانی دو تا یار (دوست دختر) داشتم یکیشون مال رشت بود و یکی شون مازندرانی، ولی من رشتیه رو دوست داشتم و دست و دلم به مازندرانی نمی‌رفت :))) بعد شروع میکنه به اون رشتیه میگه که تو دل و جان منی، راه می‌ری برام غمزه میای، دامن کوتا می‌پوشی، بهم محل نمی‌ذاری :)) دیگه ترجمه‌ی ترجیع‌بندش رو هم بیخیال :)

فردا آسمان رشت بارانی‌ست
https://open.spotify.com/episode/4DVOHKzCbcAyQ9f97Zd0BO?si=e54028ed419347a8

حالا برای اینکه حال و هواتون عوض بشه، ما خیلی وقت پیشا یک سری پست اروتیک نوشتیم توی کانال که به حرفای اخیر مربوطه. توصیه میکنم بخونیدش و از دست ندید :)

اسم این سری پست ها هست از نیوتن و تورینگ تا cyber-physical system. یادش بخیر تز ارشدم توی این حوزه بود و امیدوارم که امسال مقاله‌اش چاپ بشه :(

متأسفانه امروز توی یکی از شهرای همسایه‌ی ما یعنی شهر Strasbourg در فرانسه دو تا tram توی ایستگاه اصلی شهر با هم تصادف می‌کنند و باعث مجروح شدن ۵۰ نفر میشه که حال ۵ نفرشون وخیمه. طبق آخرین اخباری که بیرون اومده یکی از دلایل این تصادف باز شدن سوئیچ ریل یکی از track ها بوده و قطاری که داشت با سرعت تمام در جهت عقب حرکت می‌کرد به قطاری که ایستاده بود برخورد میکنه.

لینک خبر

حالا باید منتظر موند تا اخبار دقیق تری منتشر بشه منتهی همواره باید منتظر وقوع این اتفاقات تلخ باشیم تا یادآوری شه که formal methods رو باید بیشتر جدی بگیریم. اون سیستم شاید برای صدها میلیون ثانیه داشته بدون خطا کار می‌کرده، منتهی فقط کافیه میون میلیاردها میلیارد رفتار مختلفی که سیستم داره، تنها یکیش Buggy باشه و همون باعث تلفات جبران ناپذیر باشه. به هیچ وجه هیچ چیزی نمیتونه جای اثبات و تضمین بدون خطا بودن سیستم رو بگیره، نه تست، نه فاز، و نه AI

آخرین ورژن منتشر شده‌ی JMC طبق benchmark هامون میتونه یک برنامه‌ی مالتی‌ترد Java که تعداد equivalent class های Execution trace هاش ۲۵۰ هزارتاست رو توی ۱۵ دقیقه Model Check کنه. دو ماهه که با شیرینیدی refactoring و optimization این ابزار رو شروع کردیم و چیزی به انتشار نهاییش نمونده. توی نسخه‌ی جدید این زمان به کمتر از ۵ ثانیه می‌رسه و این یعنی یک قدم دیگه نزدیک شدیم به آرمانمون، Unlocking Software Model Checking :)

تصنیف آتشِ دل در کنار آلبوم عشق داند شجریان و تصنیف بهار دلکش، یکی از بی‌نظیرترین تصنیف‌هایی هستش که در دستگاه ابوعطا ساخته و اجرا شده. هر بار که گوش میدی جدید و تازه است.

ما اینجا نشستیم داریم فرمال مون رو میخونیم ولی این برف نمیذاره لعنتی. شرمنده دوربین گوشی هم کیفیتش پایینه :)

"باگ نه تنها در سافتور، بلکه در ریاضیات"
پیرو کشف یک باگ در اثبات یکی از قضایای مهم ریاضی بعد از ۶۰ سال
——————————————

با پیدایش روش‌ها فرمال برای اثبات correctness برنامه‌ها و پیدا کردن باگ و توسعه‌ی فریمورک‌ها و ابزارها، به مرور زمان کاربردهای دیگری هم برای این روش‌ها پیدا شد و یکی از اون‌ها توصیف فرمال قضایای ریاضی با این روش‌ها و اثبات درستی‌شون بود. درسته که برای هر قضیه یک اثبات وجود داره، منتهی اکثر این اثبات‌ها Machine-readable نیست و درستی‌شون توسط آدم‌هایی که اون‌ها رو خوندن تایید شده. ولی خب آدم هم اشتباه می‌کنه و شاید نتونه اگر اثبات مشکلی داره اونو پیدا کنه. آقای Kevin Buzzard از دانشگاه امپریال کالج با همکاراشون یک پروژه‌ی جاه‌طلبانه پیرامون فرمال کردن اثبات قضیه‌ی آخر فرما رو شروع کردند. اثبات این قضیه شامل برنچ‌های نوینی از ریاضیات میشه که بخش قابل توجهی ازش رو کسی Machine-readable یا فرمال نکرده. یکی از این بخش‌ها مربوط به هندسه میشه که بهش میگن crystalline cohomology. زمانی که داشتن این مفهوم رو به یک زبان فرمال machine-readable ترجمه می‌کردند، آقای Antoine Chambert-Loir از دانشگاه Paris Cité به یک اروری بر میخورن. این ارور مربوط میشد به بخشی از یک اثبات قدیمی که پایه‌های crystalline cohomology رو شکل میداد. این اثبات توسط یک ریاضی‌دان فرانسوی به نام Norbert Roby در سال ۱۹۶۵ در یک مقاله انجام شده بود و مشخص شده که اشکال داره. وقتی دقیق شدن به اثبات دریافتن که آقای Roby یادشون رفته بود یک سیمبلی رو بین دو خط قرار بدن و باعث invalid شدن اثبات شده بود. از اونجایی که برای crystalline cohomology اثبات‌هایی با استراتژی‌های مختلفی داده بودن مشکل بزرگی پیش نیومد ولی اگر تنها اثبات موجود همین اثبات آقای Roby بود اون وقت تمام کارای جدیدی که روی crystalline cohomology انجام شده بود هم زیر سوال میرفت.

بعد از اینکه آقای Buzzard این ارور رو با آقای Brian Conrad که استاد دانشگاه Stanford هستند در میون گذاشت، یک اثبات جدای درست دیگه پیدا کرد برای اون چیزی که آقای Roby قصد داشت اثبات کنه و خب این نشون داد که باگ پیدا شده به قولی Fatal Error نیست.

خلاصه این بار ارور پیدا شده خیلی خطرناک نبود ولی کسی چه میدونه که چقدر اثبات‌هایی که برای قضایا دیگه داریم درست هستند. اینجاست که ارزش‌های فرمال متد مهم میشه و نقش بازی می‌کنه.

جا داره بگم که تلاش‌ها برای فرمال کردن اثبات قضیه‌ی آخر فرما داره با استفاده از Theorem Prover Lean انجام میشه که علاوه بر ریاضیات میشه باهاش باگ‌های سافتوری هم پیدا کرد.

ما یادمون نمیره
https://www.moniravanipor.com/persian-books

بازخوانی ترانه‌ی بالا

این تصویر دو بند از نامه‌ی Dijkstra به اعضای Budget Council دپارتمانش تو دانشگاه TU Austin بوده (بخاطر تصمیم دانشکده در شیفت از زبان فانکشنال به imperative برای درس مبانی برنامه‌نویسی شون)

از همین نامه که ایشون لفظ discourages operational reasoning رو به کار برده میشه فهمید که چقدر با model checking مشکل داشته :))
متن کامل این نامه

Summer Intern @ IMDEA Software
—————————————————

یکی از فارغ التحصیلای استادم یعنی آقای Kaushik Mallik که تز دکتری‌اش با عنوان "Pushing the Barriers in Controller Synthesis for Cyber-Physical Systems" برنده‌ی جایزه‌ی ETAPS doctoral dissertation award سال ۲۰۲۳ شد که یکی از معتبرترین جایزه‌ها در حوزه‌ی TCS محسوب میشه که یک دانشجوی دکتری می‌تونه بگیره، بعد از اتمام پست‌داکش در ISTA زیر نظر آقای Thomas Henzinger، به عنوان Assistant Professor جذب موسسه‌ی IMDEA Software در مادرید شده و داره research group خودش رو دایر می‌کنه. حوزه‌ی کاریش intersection گیم تئوری، کنترل تئوری، و Formal Method هستش و این اواخر روی Monitoring سیستم‌های AI هم کار کرده. به بیان دیگه سعی ‌می‌کنه با تکنیک‌های Game Theoretic الگوریتم‌ها و فریمورک‌های فرمال برای Controller Synthesis ارائه کنه.

ایشون دنبال intern هست برای تابستون پیش‌رو و اگر علاقه‌مند هستید مهلت دارید تا ۱۰ ژانویه از طریق این لینک اپلای کنید و بهشون ایمیل بدید. در مورد موسسه‌ی IMDEA هم بارها توی کانال در موردش صحبت شده کافیه اسم IMDEA رو سرچ کنید، یک موسسه‌ی تازه تأسیس با کلی ریسرچر قوی و خوش آتیه که بسیار رو به جلو و قوی داره پیش میره.

جهت یادآوری این جلسه تا دقایقی دیگر شروع میشه.

"در ابتدا تقارن وجود داشت"
از کتاب جزء و کل به نوشته‌ی آقای Werner Heisenberg.
—————————————

چند روز پیش به یک کتاب Open Source برخورد کردم به نام SYMMETRY که چند نویسنده داره و من یکیشون رو یعنی Ulrik Buchholtz رو می‌شناختم. از اونجایی که ایشون Type theory کار هستند، حس کردم کتاب باید حرف تازه‌ای برای گفتن داشته باشه. وقتی که راجع به باقی نویسنده‌های کتاب سرچ کردم فهمیدم که کتاب رو تعدادی TCS کار نوشتن و همونطور که میشه از بکگراند حضرات حدس زد، کتاب بر پایه‌ی univalent mathematics پیش میره و سعی در تعریف یک Foundation برای پاسخ به سوالات مرتبط با Symmetry داره. کتاب با type theory شروع میشه، از group theory عبور می‌کنه، دستی به Automata Theory میده و به تئوری گالوا میرسه. شاید بد نباشه که کمی شفاف کنم که چرا چنین مبحثی برای شخص خودم اهمیت داره.

بر خلاف خیلی از دوستانی که در ماهای گذشته به جمع ما پیوستن، من رشته‌ام ریاضی نیست. اما خب توی Theoretical of computer science به خطوط Track B کانسپت Symmetry و مشتقاتش خیلی به دادمون میرسه. مثلا ما یک دنیایی داریم توی این track به اسم Abstract Interpretation که PL ای‌ها و Compiler ای‌ها ازش خیلی استفاده می‌کنند. به لطف روپاک و رفقاش، verification ای ها هم از ۲۰۰۰ به اینور ازش استفاده می‌کنند. کانسپت Abstract Interpretation برای اولین بار توسط آقایان Patrick Cousot و Radhia Cousot در دهه ۷۰ میلادی معرفی شد. Semantics فرمالی که این بزرگرواران در دو مقاله‌ی معروف و فوق العاده پیچیده‌شون ارائه دادند بر پایه‌ی Lattice Theory و Galois connections بود. یکی دیگه از کاربردای Symmetry توی Model Checking هستش. خیلی از سیستم‌های Concurrent ای که ما میخوایم verify شون کنیم، تشکیل شده از process هایی هستند که رفتار identical دارند و با تعریف یک symmetry reduction ای که sound باشه میشه فضای حالت سیستم رو به شدت کاهش داد. یک نسخه‌ی Generalized شده‌ی Symmetry به ما در verify کردن parameterized concurrent system ها کمک می‌کنه بدین صورت که اگر اثبات کنیم سیستم به‌ازای تعداد مشخصی process وریفای میشه، میشه نتیجه گرفت که به ازای بینهایت process هم وریفای میشه و به ما در verify کردن infinite state systems ها کمک میکنه.

اینها رو گفتم تا بیشتر دید بدم بهتون ولی خودم دنبال چیز دیگه‌ای از Symmetry هستم. یکی از پروژه‌هایی که روی JMC نعریف کردیم، verify کردن distributed system هایی هستش که با پترن Executors/Futures کار می‌کنند. بدین صورت که شما یک Executor دارید که تشکیل شده از یک Thread Pool و یک Runnable Queue هستش و یک سری Task رو به این Executor سابمیت می‌کنید. وقتی که ما اومدیم این پترن رو به شکل فرمال مدل کردیم و بهش یک semantics مبتنی بر dynamic partial order reduction دادیم، دریافتیم که فضای حالت به شکل سوپرنمایی بزرگ میشه وریفای کردنش خیلی راحت نیست. الان دنبال این هستم که بتونم با توسعه و افزودن یک symmetry reduction به این partial order reduction یک تکنیک sound داشته باشم برای کاهش دادن فضای حالت تا بتونیم یک subclass از این مسائل رو به شکل موثری verify کنیم.

از این جهت این کتاب برام جذاب اومد و گفتم که به شما هم معرفیش کنم. نکته‌ای که هست اینه که این کتاب در درست نگارشه و برخی از فصل‌هاش خصوصا فصول انتهاییش کامل نیست. ولی آخرین ورژن Draft این کتاب رو میتونید از طریق این لینک دسترسی داشته باشید. لینک ریپوی این کتاب هم اینجاست.

عنوان پست، جمله‌ای هست که روی جلد کتاب نوشته شده.

فردا در آخرین جلسه‌ی کلاس نظریه‌ی زبان‌ها و ماشین‌ها که به صورت مجازی برگزار خواهد شد، برای گفت‌وگو درخصوص مطالب پیشرفته‌تر و پژوهش در حوزه‌ی روش‌های صوری و ارتباط آن با دیگر حوزه‌های علوم کامپیوتر، میزبان خانم دکتر مرجان سیرجانی، پژوهشگر و استاد برجسته‌ی علوم کامپیوتر دانشگاه Mälardalens سوئد خواهیم بود.

بخشی از دیگر سوابق ایشان:

- استاد دانشکده‌ی مهندسی برق و کامپیوتر، دانشکده‌ی فنی دانشگاه تهران
- پژوهشگر ارشد، پژوهشگاه دانش‌های بنیادی (IPM)
- پژوهشگر مهمان، دانشگاه California, Berkeley
- پژوهشگر مهمان، دانشگاه Illinois at Urbana-Champaign
- موسس و رئیس کمیته‌ی راهبری کنفرانس FSEN
- رئیس کمیته‌ی برنامه‌ریزی کنفرانس‌های SEFM و COORDINATION

این جلسه فردا پنج‌شنبه ۱۳ دی‌ماه از ساعت 10:30 صبح تا 12 در لینک زیر برگزار خواهد شد.

https://vc.sharif.edu/ch/pdl

لطفا پس از ورود به لینک، از طریق گزینه‌ی مهمان وارد شوید و نام و نام خانوادگی خود را وارد کنید. شرکت برای عموم دانشجوها بلامانع است.

با آرزوی سلامتی و موفقیت
معینی‌جم

آقااااا :))) من اینو دستم خورد اینجا فرستاده شد :))
کلا هر پستی میاد اینجا یک ساعت وایسید بعد بخونید من یکم بد دستم تو تلگرام :))

من قدیما ممبرای کانالم سی چهل تا بود کلا و همه هم دوستام بودن مهران و مهدی و حسین و مهسا و ساغر و مریم و رضا و پسرداییم و سروش و تعدادی از دوستای کارشناسیم برای همین پست‌ها و مطالب اروتیک میذاشتم هر از چندگاهی فضا یکم از این فرمال سمی خارج بشه اما از وقتی که ممبرا زیاد شد و مثلا استادای دانشگاهمم جوین شدن دیگه حیا میکنم و از این حرفا نمیزنم

حالا امشبم چون شب سال نو هستش پاک نمیکنم و باشه به یاد ایام قدیم :) ولی دیگه از این خبرا نخواهد بود :)

@Eunoia

مستندی کوتاه و جذاب درباره دکتر محمودیان

امسال هم به مانند ۲۷ ادوار گذشته، آقای Donald Knuth لکچر معروفی که هر سال به مناسبت کریسمس برگزار می‌کنند رو در دانشگاه استنفورد برگزار کردند. در ۲۸ امین Christmas lecture شون به محاسبه‌ی weak و strong components روی یک گراف جهت‌دار پرداختند. برای محاسبه‌ی این مسئله الگوریتم معروف آقای Robert Tarjan رو بحث میکنند که طبق گفته خود آقای knuth این الگوریتم جالب‌ترین الگوریتمی بوده که در طول زندگی‌شون تا به حال باهاش برخورد کردند.

لینک این لکچر رو میتونید در اینجا پیدا کنید.

ذاتِ Turing

آقای Matt Might زمانی که هنوز توی آکادمیک بودن و دانشگاه Utah استاد بودن، توی درس Advanced Compiler Design شون، تو بازه‌ی Halloween یه چیزی داشتن به اسم Halloween Lecture و توی اون لکچر در مورد cpp templates صحبت می‌کردند و اثبات می‌کردند که Turing-complete هستند. توی این لینک نحوه‌ی اثبات جالبشون رو می‌تونید بخونید.

فکتِ شب

تمپلِیت متا پروگرامینگ Turing-complete است.

شب بخیر

قدیم‌ترها کلی توی کانال در مورد Proof-oriented programming صحبت کردیم. فکر کنم توی این پست، که آخرین صحبت‌های تکمیلی ما بود، لینک تمام پست‌های مربوط به این تاپیک رو گذاشتم. امروز یه کتاب مرتبط دیدم از آقای Ilya Sergey با عنوان Programs and Proofs Mechanizing Mathematics with Dependent Types که بهونه‌ای دستم داد تا هم یادی از اون مباحث کنم و هم این کتاب رو بهتون معرفی کنم. این کتاب در حقیقت Lecture Note هایی بوده که ایشون درس میدادن.

خیلی ها بیخیال نشدن. و خب به لطف بیخیال نشدن این عزیزان ما امروزه foundation مناسبی برای توسعه‌ی تکنیک‌های software model checking داریم. حالا اگر طبق عادتم دوباره نرفتم توی یک غیبت طولانی، براتون اولین تلاش‌ها برای رفع این مشکل رو توضیح میدم و می‌بینیم که چطور با ارائه چند تکنیک ساده تونستن model checker ای بسازن به اسم SPIN که با گذشت بیش از ۳۰ سال هنوزم یکی از قوی‌ترین ابزارهای verification برنامه‌های distributed و multi-thread هستش.

مسئله‌ی Reachability با تمام سادگیش، مسئله‌ی Hard ای محسوب میشه و توی ترک B تئوری علوم کامپیوتر اگر نگم مهم ترین، ولی یکی از مهم‌ترین مسائلی هست که پاسخ دادنش در هر setting ای ارزش بالایی داره.

به شکلی که ما یک کنفرانسی داریم به نام Reachability problems conference یا به اختصار RP که ۱۸ ساله داره برگزار میشه.

این کنفرانس برای ۱۹ امین سال قراره که توی سال ۲۰۲۵ در موسسه‌ی IMDEA software واقع در شهر مادرید برگزار بشه و ددلاین ارسال مقاله‌اش هم ۶ ماهه دیگه. اگر شما هم این موضوع براتون جذابیت بالایی داره، give it a shot و سعی کنید یه چیزی برای این کنفرانس آماده کنید.

https://rp25.software.imdea.org/index.html

گوشه‌هایی از شهر Cochem

یه چیز خوب دیگه‌ای که دیدم این بود که آقای Loris D'Antoni و خانم Nadia Polikarpova از UCSD که تو حوزه‌ی Program Synthesis خیلی آدمای قوی‌ای هستند، اسلایدها و کتابی که با هم نوشتن برای کورس Program Synthesis شون رو توی گیتهاب پابلیک کردن. خیلی منبع خوبیه به نظرم برای کسی که میخواد با این حوزه آشنا بشه. لینک کورس آقای لویس اینجا و لینک کورس خانم نادیا اینحاست.

آقا راستی امسال دکتر ایزدی Theory of Computation ارائه داده‌اند و دیدم که یک راهنما درست کردن برای دانشجوهاشون که هر مبحث رو از کجا بخونن و خیلی به نظرم حرکت قشنگی بود چرا که حتی اگر کسی میخواد سلف استادی بخونه میتونه به عنوان یک guide line ازش استفاده کنه. از اینجا میتونید به این فایل دسترسی پیدا کنید.

راستی آقا چقدر بچه‌های Irif تو Concurrency Theory قوین. و خیلی خوشحالم که شیرینیدی و لوسی اومدن موسسه‌مون تاک دادن و باب همکاری باز شد. از Irif خوشمان آمد.

آقا پارسال شب ددلاین Concur بود که مقاله رو نوشته بودم و داشتم هی مرورش میکردم که یه وقت مشکلی نداشته باشه. بعد دیدم مهسا سرش خلوته، نشوندمش و با استفاده از تکنیک Rubber duck debugging سعی کردم اثبات هام رو مرور کنم. یه وقت به خودم اومدم دیدم اثبات complete بودن سیستمم sound نیست و دنیا رو سرم خراب شد. همونجا ها بود که این جمله رو با تمام پوست و استخون درک کردم. حالا ددلاین Concur امسال مشخص شده و ۳ ماه دیگه است و امروز نشستم یه دور پیپرم رو خوندم و واقعا هیچ ایده‌ای نداشتم که این پیپر رو کی نوشته :)
خلاصه امیدوارم بتونم بدون relax کردن مسئله اثبات رو درست کنم و دیگه جدی امسال این کار رو بدم و هر چه زودتر از شرش راحت شم

PhD in Semantics @ Kent Univeristy
—————————————————

Marco Paviotti: Dear all,

I am looking for a #PhD student to work on (any subset of) these topics:
#semantics, #domaintheory, #categorytheory #typetheory and #functional programming.

Deadline for application is 15th of February 2025.

here's the official call: https://kent.ac.uk/scholarships/search/FN15COMPGR01

توصیه میکنم قبلا ارتباط با ایشون این صفحه رو هم بخونید.

توی این کامنت فربد لینک یک‌سری از کنفرانس‌های سیستمی رو معرفی می‌کنه که اخیرا در حوزه‌ی سیستم برگزار شدن و یک session منحصر به فرمال متد داشتند. به علاقه‌مندان این دو حوزه بسیار توصیه میشه.

اخیرا دارم با کامیونیتی سیستم کارها مشکل اساسی پیدا میکنم. البته با تمام احترامی که برای دوستان سیستم کارم دارم، خصوصا فربد جان، ولی جدی این غرور مزخرفی که دارن نسبت به اینکه ما چقدر خفنیم و فقط ما داریم کار درست حسابی انجام میدیم و باقی‌تون دارید اسباب بازی میسازید رو درک نمیکنم که از کجا نشأت میگیره. هر وقت من توی یه ایونتی باهاشون هم کلام میشم و حرف از مدل چکینگ میزنم با یک لبخند تمسخر آمیز گوشه‌ی لب مزخرفشون میگن که خب تهش میخواید با Halting problem چیکار کنید ؟ :) یعنی حضرت عباسی اگر تو عمرشون یک بار ماشین تورینگ کشیده باشن یا اصلا بفهمن که آقا برنامه‌های چرندی که می‌نویسید و با هزار دوز و کلک به حلق کامیونیتی تون میتپونید رو میشه با یک استیت ماشین فاینایت مدل کرد. هی هم میگن خب اگر سایز برنامه بزرگ بشه که نمیتونید وریفای کنید. حالا خوبه زیر همون یدونه verifier ای که برای ebpf شون نوشتن موندن و دست به دامن کامیونیتی ما شدن.
جدی یک تو دهنی محکم براشون رفت توی todo لیستم. مطمئن باشن که سیلی خواهند خورد، شاید نه فورا ولی حتما

داشتم یه مطلب درباره برندگان جایزه تورینگ می خوندم. به نوبل علوم کامپیوتر معروف هست. از ۱۹۶۶ جایزه اش رو دارند اهدا می کنند. موضوع مقاله بررسی شرایط اجتماعی برندگان هست. کمی طولانی هست و جزئیات زیاد داره. رفته پیشینه برندگان رو بررسی کرده، خانواده، دانشگاه و هر چی که فکرش رو بکنید. ظاهرا بهش می گند
prosopography
فارسی اش می شه، خاستگاه شناسی.
بعضی از نتایج و نکته ها که تا اینجا خوندم، اینجوری بوده:
*برنده ها از خانواده های متوسط یا بالاتر بودند. پدر و مادر تحصیلات بالا و از این چیزها.
*ارتباط و شبکه سازی و ... از این چیزها تاثیرگذار بوده. نه به معنای بد. این شاگرد فلانی بوده، اون چون یه بار فلانی رو دیده بوده با مساله یا مسیر جدیدی آشنا می شه و از این چیزها. همکاری های علمی و ...
*آمریکا و یه سری از  دانشگاه های خاص اون درصدر هستند و ...
* برندگان بیشترشون علوم کامپیوتر نخونده بودند!
*بحث های قومی و نژادی، جنسیت برندگان(فقط سه زن برنده شدند تا حالا و اون هم برای سال های اخیر بوده)
*اینکه مثلا گوگل حمایت مالی می کرده یه سال هایی رو و بعضی از برندگان همکاری داشتند با گوگل و از این حرف ها...
* ۱۲ تا از برندگان اصلا phd نداشتند، چند تا از برندگان اصلا علوم پایه یا مهندسی نخوندند و مثلا رشته شون علوم سیاسی بوده!
*فقط یه آسیایی جایزه رو برده اون هم چینی.

صفحاتش زیاده و نکات ریز و درشت زیادی رو گفته، که جالب به نظر میاد. بعدا شاید نکات دیگه ای رو گذاشتم.

 لینک:
https://shs.hal.science/halshs-01814132/

زبان گیلکی، چیزی که مدت‌هاست از گوش و زبانم به دور بوده.

PhD in Arithmetic of Periods @ MPI-SWS & Leiden
————————————————————

دو تا پوزیشن دکتری هست در حوزه‌ی Arithmetic of Periods که جوینت موسسه‌ی مکس پلانک و دانشگاه لایدن هلند باز شده. پروژه‌ها یک جورایی intersection محاسبات و هندسه‌ی جبری هستن. برای همین یک فرصت بسیار خوبی میتونه برای بچه‌هایی باشه که ریاضی محض کار کردن و دوست دارن وارد TCS هم بشن. علاوه بر Joel از MPI و آقای EMRE SERTÖZ از لایدن، آقای James Worrell از آکسفورد هم co-supervisor این پوزیشن‌ها خواهند بود و این فرصت برای فرد فراهم میشه که در سال یک ماه رو آکسفورد باشه.

ددلاینش ۱۵ ژانویه است و برای کسب اطلاعات بیشتر به این لینک مراجعه کنید.

یکی از بزرگترین دست آوردهایی که در اروپا آنلاک کردم، یاد گرفتن درست کردن خمیر پیتزا به شکلی بود که از آندرا نمره‌ی قبولی بگیره. دوم آشنایی با پنیرهای ایتالیایی و کاربردشون در پخت پاستا و پیتزا بود. پنیر هایی مثل Pecorino، Ricotta, Burrata و fior di latte رو دستم اومده. سوم آشنایی با شراب‌هاشون و به نظرم تا اینجا از فرانسوی ها بهترن (شاید البته روزی به این نتیجه برسم که حریف château نمیشن )

امیدوارم همینقدر که اعتماد به نفسم داره توی آشپزی بالامیره، توی حل مسئله‌ی safety verification سیستم‌های non-atomic network که پراسس‌هاش با Rendez-vous با هم تعامل می‌کنن هم بالا بره

Austin Tuesday Afternoon Club 1990

اولین نفر از چپ که جلوی میز نشسته و کت تک پوشیده آقای Emerson هستند و اون شخصی که جلوی تخته نشسته با پیراهن سفید و عینک دارند Dijkstra

“Sir, you are at risk of winning the argument.”
برای مرحوم E. Allen Emerson
—————————————————————
دو روز بعد اینکه تصمیم گرفتم در اینجا رو تخته کنم، یعنی ۱۶ اکتبر، توی توییتر دیدم که آقای Rajeev Alur اعلام کردند که متأسفانه آقای E. Allen Emerson فوت کردند. یادم میاد که روز خیلی تلخی بود اون روز. من از روزی که به شکل جدی وارد آکادمیک شدم همواره مشغول کار روی Model Checking بودم و حالا می‌بینم که دومین نفر از سه نفری که شروع کننده‌ی این داستان بودن فوت کردند. یادمه هفته بعدش یعنی ۲۳ اکتبر که روپاک سر کلاس Software Verification مبحث Enumerative Model Checking رو تموم کرد، درب ماژیک رو بست و بعد از چند ثانیه سکوت همراه با افسوس رو به ما کرد و گفت که جا داره یادی کنیم از Emerson که متأسفانه هفته پیش فوت کردند. واقعا از دست دادن ایشون یک افسوس بزرگ برای حوزه‌ی ما خواهد بود، من در کنفرانس‌های زیادی ایشون رو دیدم و باهاشون صحبت کردم و واقعا نمیدونم چطور بگم که چقدر انسان دوست داشتنی‌ای بودند.
دوست داشتم همون روزی که این خبر رو فهمیدم بیام اینجا و چیزی بنویسم. همونطور که حدس می‌زدم هیچ یک از دوستان در کانال‌هاشون سخن و اشاره‌ای به این خبر نداشتند و این غم لابه‌لای خیلی از سخن‌ها و خبر‌های شاید مهم‌تر محو شد. تا اینکه امروز یک سر ستون در والیوم ۶۷ ام مجله‌ی CACM که ۵ روز پیش منتشر شد خوندم که یادواره‌ی آقای Emerson بود و بهانه‌ای دستم داد تا این خبر تلخ رو غبار روبی کنم.
آقای Allem Emerson زمانی که در Harvard دکتری‌شون رو با آقای Edmund Clarke شروع کردند تصمیم گرفتن که تز دکتری‌شون رو معطوف کنند به Verification ویژگی‌های فرمال‌شده روی سیستم‌های Finite-state. تقریبا یک روز که ایشون داشتن با Clarke در حیاط محوطه‌ی Harvard قدم میزدن، اصطلاح Model Checking رو خلق کردند. ۲۵ سال بعد به پاس تلاش‌های ایشون و آقای Clarke و آقای Joseph Sifakis برای خلق و توسعه‌ی Model Checking و کاربرد موثر این تکنیک در Verification نرم‌افزارها و سخت‌افزارها، به هر سه‌ی این عزیزان جایزه‌ی Turing Award اهدا شد. آقای Clarke متأسفانه در سال ۲۰۱۹ بر اثر ابتلا به بیماری کرونا فوت کردند و حالا هم نوبت به اولین دانشجوی دکتری‌شون رسید. شاید حالا که از آقای Clarke یادی کردیم، اشاره‌ای کنیم به پستی با عنوان "صفحات پایانی ۳".
آقای Emerson دو منبع مهم الهام‌شون برای توسعه‌ی مدل چکینگ رو مقاله‌ی Proof of a Program : Find نوشته‌ی آقای Tony Hoare و یک سخنرانی از آقای Zohar Manna با عنوان Fixpoints and the Tarski-Knaster Theorem عنوان کردند. حالا که اسم این بزرگواران رو آوردم، بد نیست که ارجاع بدم شما رو به دو پست "ارمغان پیری" و "زهر منا".
آقای Emerson بعد از اتمام دکتری‌شون، وارد دپارتمان CS دانشگاه TU Austin در تگزاس شدند. جایی که آقای Edsger Dijkstra هم حضور داشتند و یکی از مخالفین سر سخت Model Checking بودند. حالا که یادی از دایکسترا شد همینجا شما رو ارجاع میدم به خوندن پست "واحد اندازه‌گیری غرور : نانو Dijkstra" در کانال. او معتقد بود که برنامه نویس‌ها خودشون باید در مورد درستی برنامه‌شون reasoning کنند و نباید روی ابزار‌های Automated Program Checker اتکا کنند. سال ۱۹۸۵ آقای Emerson مقاله‌ای رو با عنوان Modalities for model checking (extended abstract): branching time strikes back در کنفرانس POPL منتشر می‌کنند. آقای Dijkstra در اون سال در یکی از جلسات معروف Austin Tuesday Afternoon Club شون تصمیم می‌گیرند که به بررسی این مقاله بپردازن. همینجا شما رو ارجاع میدم به خواندن پستی که قدیما با عنوان "کلوب سه شنبه ها، بعد از ظهر" منتشر کردم.
توی اون جلسه آقای دایکسترا شروع می‌کنند به نقد این مقاله و نقدشون رو در قالب یک یادداشت تند برای آقای Emerson می‌نویسند، یک هفته بعد آقای Emerson به عنوان جوابیه یک یادداشت برای آقای دایکسترا می‌نویسند و تمام حملات آقای دایکسترا رو جواب میدن. آقای دایکسترا در نهایت می‌پذیرند که نقدهاشون نادرست بوده و با آقای Emerson دوست صمیمی میشن. آقای Emerson میگن که آقای دایکسترا واقعا به مفید بودن Model Checking پی بردند و با اون غرور معروفی که داشتند یه روز به آقای Emerson میگن :
“Sir, you are at risk of winning the argument.”
خیلی برام سخته که می‌بینم دارم تو حوزه‌ای کار میکنم که اکثر pioneer هاش دیگه بین ما نیستن. از بین تمام افرادی که توی این پست ازشون یاد کردم فقط دو سه نفرشون زنده‌اند. امیدوارم قبل از اینکه نوبت به من هم برسه بتونم روزی به هدفی که در ابتدای دکتری برای خودم تعیین کردم برسم، Unblocking Software Model Checking.
با این شعر از سایه خاتمه بدیم.
نآمدگان و رفتگان از دو کرانه‌ی زمان
سوی تو می‌دوند هان! ای تو همیشه در میان

سروش برام فرستاد
همیشه استاد، استاد روحانی

یکم ماه، موعد پرداخت کرایه خونه‌مونه. همیشه یکم ماه اولین دیالوگی که بین من و مهسا برقرار میشه اینه که
- پول صاحبخونه رو زدی؟
+ [ آره ریمایندر ست کرده بودم | نه الان میزنم ]
دیروز بعد این دیالوگ یادمون اومد که ۲۲ ام اکتبر سال پیش بود که با صاحبخونه قرار گذاشتیم که بیایم خونه رو ببینیم. یادمه که پیدا کردن خونه توی مرکز شهر و بخصوص اونجایی که مردم محلی بیشتر زندگی می‌کنند کار سختی بود. بیشتر خونه هایی که توی این محل ها بودن رو وقتی به مالکش پیام می‌دادیم جواب نمیدادن. صاحبخونه ما هم اولش جوابمون رو نداد. من توی لینکدین پیداش کردم و بهش اونجا پیام دادم. رفت پروفایلم رو دید و بعدش بهمون زنگ زد که من ۲۲ اکتبر زاربروکن هستم و ساعت ۲ بیاید خونه رو ببینید. اون روز مهسا گفت بیا خوش سر و تیپ بریم که ایمپرشن مثبت بذاریم روی طرف. وقتی رسیدیم جلوی درب ساختمون دیدم که صاحبخونه مون داره از سر چهارراه میاد به سمت آپارتمان و سر و تیپ اون خیلی خیلی لاکچری و classy بود جوری که به نظرم اومد اونم میخواست روی ما ایمپرشن مثبت بذاره :)
یادمه تو بین صحبتمون باهاش بهمون گفت که یک دوست خانم ایرانی داره و خلاصه خدا رو شکر دیدگاه بسیار خوب و لطیفی نسبت به ایرانیا داشت. ما هم به محض اینکه داخل خونه رو دیدیم یک دل نه صد دل عاشقش شدیم و گفتیم که هر چه زودتر میخوایم قرار داد رو ببندیم. هفته بعدش رفتیم قراداد رو بستیم و یکم نوامبر از Guest house مکس پلانک به خونه مون نقل مکان کردیم. با این حساب دقیقا یک سال از اومدن مون به این خونه میگذره و علاوه بر خانواده‌ و دوستام، خیلی دلتنگ کتابام هستم. بخصوص کتاب شعرام. بعضی وقتا که با خانواده‌ام صحبت میکنم مادرم گوشی رو میبره تو اتاق خوابم و کتابخونه‌ام رو بهم نشون میده و میگه هر از چندگاهی گردگیری شون میکنم. از اونجایی که میدونم چند سالی بیشتر قرار نیست اینجا ساکن باشیم، دوست ندارم با آوردن و یا خریدن کتابام خودمون رو توی دردسر جابه‌جاییش بندازم. هر از چندگاهی که دلم براشون تنگ میشه، مثل خوانواده و دوستام، آخرین عکسی که ازشون شب رفتنم گرفتم و نگاه میکنم.

ما بالاخره بعد ۶ ماه، تمام commit های داخلی پروژه‌ی JMC رو پوش کردیم روی برنچ main که به شکل public از طریق این لینک قابل دسترس هستش

https://github.com/mpi-sws-rse/jmc

نسبت به نسخه‌ی قبلی feature های بسیاری اضافه کردیم. منتهی readme آپدیت نیست و به‌زودی آپدیتش میکنم.

خوشحال میشم که یک امتحانی بهش بدید و سعی کنید build کنید و اگر موردی بود بهم بگید. توصیه میکنم روی IntelliJ بیلد کنید.

سلام به دوستان و همراهان عزیز

حقیقتا صحبت‌های بنده در روزهای گذشته بازتاب‌هایی داشت و تعداد خوبی از این بازتاب‌ها رو هم در کانال‌های دوستان یا در جاهای دیگری خوندم. حقیقتا از خیلی از این افراد، یک شناخت نسبی و یا عمیق بر اساس نگرش و بینشی که دارند از پیش داشتم و متوجه شدم که شناختم خیلی درست نبوده، بنده توقع خردمندی، نکته‌سنجی، و معرفت بیشتری داشتم از این عزیزان ولی خود غلط بود آنچه می‌پنداشتیم.

مصرم بر اینکه هیچ یک از حرفای بنده، ساده‌انگاری، بی‌اخلاقی، غیر حرفه‌ای، متعصبانه، مغرضانه، و یا عناوین دیگری که این دوستان لطف کردند و به بنده نسبت دادند نبوده و قصد داشتم راجع به هر بخش جداگانه شرح بدم و صحبت کنم. منتهی با خودم فکر کردم که من سال‌هاست اینجا دارم مینویسم و هر بار مجبورم از حرفام دفاع کنم و در آخر هم چیزی تغییر نمیکنه، درست عین آدم‌ها.

خلاصه تصمیم دارم که بعد این همه نوشتن بی‌اثر و بی ثمر، برای مدتی طولانی فاصله بگیرم از این فضا و سعی کنم کار دیگری که فکر میکنم مفیدتره انجام بدم. به طور خاص استراحت کردن و از زندگی لذت بردن.

اینجا رو نگه میدارم تا دسترسی دوستان به مطالب گذشته حفظ بشه.

در انتها چند کانال رو که به نظرم ارزش دنبال کردند دارن بهتون معرفی میکنم.

خود گفته‌ها
Annie's Daily
Dutchman Daily
نوشته‌های ترمینالی
Agora
Singular Thinker
آتامتاک
نگار می‌گوید که

کانال‌های خواندنی‌ای هستند و به یقین با دنبال کردنشون جای خالی ما حس نمیشه.

ارادت

آقا اینو گذاشتم اینجا تا سر فرصت راجع بهش صحبت کنم
نقدا تا فرصت کنم بنویسم این پست رو بد نیست که بخونید.

Computer science

دوستان بنده این توئیت آقای Marcel Böhme رو مغتنم می‌شمارم و یادآور میشم که ددلاین پروگرام اینترنشیپ مکس پلانک ۱ نوامبر هستش.

How does it feel like to do world-class research? If you are a CS undergrad who is interested in our topics, the Software Security group at #MPI_SP is hiring interns for summer & winter 2025!

Details:
📅 01 November 2024
✍️ cis.mpg.de/internships/
🛡️ mpi-softsec.github.io

خانم Yixin Zou هم از MPI-SP در توئیتی اعلام کردند که دنبال intern هستند برای تابستون ۲۰۲۵

یه داستانی که پیش اومده اینه که چند تا از هم آزمایشگاهی‌های من توی مکس پلانک، جولای رفته بودن Estonia که Autobóz 2024 رو شرکت کنن. اونجا با یکی از دوستای من، امید که خدا بگم چیکارش کنه :)) آشنا میشن و متوجه میشن من همچین کانالی دارم و عضو کانال میشن. هر چی هم بهشون گفتم که من اینجا فارسی می‌نویسم و شما که فارسی بلد نیستید افاقه نکرد و گفتن که ترجمه می‌کنیم می‌خونیم :) حالا این رو نوشتم گذاشتم اینجا ببینم واقعا میخونن اینایی که می‌نویسم رو یا همین طور الکی فقط می‌خواستن منو دست بندازن :)

بهتره اصلا در نوبل شیمی رو باز نکنیم. این بنده خداها در سال‌های گذشته از اینکه جایزه فیلدشون رو بیولوژیست‌ها میبردن به قدر کافی فشار خوردن. حالا امسال علاوه بر بیولوژی، فشار AI هم دارن میخورن.

حالا موضوع تاک ایشون منو یاد نقدی انداخت که دوست دارم یک روز درباره‌ی سیلابس مورد تدریس درس نظریه‌ زبان‌ها و آتوماتا توی ایران بنویسم. من اولین مواجه‌ام با آتوماتا تئوری تو اروپا بهم اثبات کرد که متأسفانه تمرکز سیلابس این درس توی ایران بیشتر تاکید روی مباحث حاشیه‌ایه. سبک و شیوه‌ی برخورد اهل فنِ آتوماتا در اروپا کاملا متفاوته. خلاصه بگم که سیپسر رو خیلی قبول ندارن و سبک خاص خودشون رو دارن که حتما توی یک پستی جداگانه بهش می‌پردازم. البته علاوه بر سیستم آکادمیک، این نقد به دانشجوها هم وارده که خیلی دنبال درک عمیق و درستی از این درس نیستن. الان مثلا تعداد دانشجوهای کلاس یک استادی که نه کارش آتوماتاست و نه درک و شناخت درستی از آتوماتا داره و نه به نظرم دوست داره که داشته باشه :))) دو برابر بچه‌های کلاس آتوماتای مهران هستش. خود همین پدیده نشون دهنده‌ی اینه که سیستم خیلی عقب وایساده و دانشجوها از سیستم عقب تر. بگذریم

دوستان فردا آقای Jacques Sakarovitc قراره در موسسه‌ی IMDEA Software یک تاک خیلی جذاب داشته باشند با عنوان “The transformation of regular expressions into finite automata: old and new results”. احتمالا دوستانی که درس تئوری آتوماتا رو پاس کرده باشند با الگوریتم تبدیل یک regex به یک finite automaton و عکسش رو آشنا هستند از همین جهت احتمالا خیلی‌هاتون بکگراند کافی رو داشته باشید. فقط حواستون باشه اروپایی‌ها به زبان‌های منظم میگن Rational languages :)
این تاک فردا پنج شنبه ساعت ۱۲:۳۰ به وقت ایران برگزار میشه که می‌تونید از طریق این لینک به شکل رایگان شرکت کنید.آقای ساکاروویچ یکی از وزنه‌های آتوماتا هستند. من اولین بار با کتاب بی‌نظیری که نوشتند یعنی Elements of Automata Theory آشنا شدم. این کتاب در مقام مقایسه با کتاب سیپسر بر خلاف اسمش اصلا مقدماتی نیست و خیلی مطالب پیشرفته‌ای داره. کتاب اولین بار به زبان فرانسوی نوشته شده و بعدا به انگلیسی ترجمه شده. آقای ساکاروویچ نوتیشن‌های خاص خودشون رو دارن برای توصیف مباحث آتوماتا و کمی با نوتیشن‌های معمولی که دانشجوها تو ایران می‌خونن متفاوته. ایشون توی جلد اول کتاب Handbook of Automata Theory یک فصلی رو نوشتند با عنوان Automata and rational expressions که به نظرم خیلی از مطالب تاک فرداشون رو پوشش میده و اگر فرصت داشتید حتما بخونید. اگر هم دسترسی به دو کتاب ذکر شده نداشتید بهم پیام بدید می‌فرستم براتون.
پسورد ورود به zoom هست :
@s3

:)

دپارتمان‌های فیزیک : چشم عباس آقا.

در راستای دهن کجی Nobel Foundation به جامعه‌ی آکادمیک فیزیک، توصیه می‌کنم اگر سال دیگه هم حوصله نداشتید کارای بنیادی فیزیکدانان رو بررسی کنید و یا خواستید تاپیک رو از ML تغییر بدید، یک نگاهی به این مقاله‌‌ی آقای لمپورت بندازید :) ایشون توی این مقاله تفسیرشون رو از نحوه‌ی تعاملات پراسس‌ها در یک محیط توزیع‌شده، بر اساس نسبیت خاص تعریف می‌کنند و ادعای رابطه‌ی Totally ordered بین تعاملات پراسس‌ها رو رد میکنن. همین نظریه، تبدیل به پایه‌ی نظریه‌ی سیستم‌های توزیع شده میشه! از طرفی، علاوه بر ML، بلاک‌چین هم هنوز هایپش بالاست و می‌تونید توی پوستر بزنید :
"for foundational discoveries and inventions that enable blockchain with consensus algorithm"

راستی ما یک بار توی کانال در قالب یک پستی با عنوان "پر cite ترین مقاله‌ی لمپورت" راجع به این مقاله صحبت کردیم. توصیه‌ میکنم بخونید حتما :)

البته من یک اشتباهی کردم و آقای Herbert A. Simon اولین کسی بودن که هم تورینگ بردن و هم نوبل. ولی ایشون نوبل شون تو اقتصاد بود!

بالاخره می‌تونیم بگیم که یک برنده‌ی جایزه‌ی تورینگ داریم که یک نوبل واقعی هم تو زندگیش برده :) اونم تو فیزیک :)

"Dov Gabbay Prize for Logic and Foundations 2024"
————————————————

سر آقای Dov Gabbay سلامت باشه. دو سال پیش به مناسبت تولد ۷۷ سالگی شون، یک جایزه‌ای رو شروع کردن به اهدای سالانه به نام Dov Gabbay Prize که به افرادی که در حوزه‌ی منطق کار میکنن داده میشه. امسال دومین سالی هست که این جایزه رو اهدا میکنن و برندگان جایزه به خاطر حل یک open problem صد ساله این جایزه رو دریافت کردند. در ادامه جزئیات این خبر رو به همراه مقاله‌ای که منجر به حل این مسئله شد رو براتون قرار میدم.

The Jury is pleased to announce that the prize shall be awarded jointly to David Asperó (University of East Anglia, UK) and Ralf Schindler (University of Münster, Germany) for their work in the foundations of set theory, and in particular for their work connecting determinacy principles and so-called strong forcing axioms, both impinging on the nature of the continuum hypothesis (the continuum having size $\aleph_2$ as a consequence from examples of hypotheses in both directions here). Principally the award is given for their solution to the decades old problem in the area by showing that there is a concrete bridge between these two rather different approaches to the foundations of set theory. This work appeared in their paper (Martin’s Maximum^{++} implies Woodin’s Axiom) in the Annals of Mathematics 2021.

David Asperó is well known for his work in set theory, in particular for his contributions to forcing and forcing axioms.

Ralf Schindler has made significant contributions to the theory of inner models of set theory under strong theoretical axioms of infinity and hypotheses of the determinacy of infinite games.

The Dov Gabbay Prize for Logic and Foundations is an international research prize launched on the occasion of Professor Dov Gabbay's 77th birthday. This initiative honours the extraordinary and multi-faceted scientific and editorial work of Dov Gabbay, known in particular for editing an extensive collection of specialized Logic Handbooks.

این عکس رو خیلی رندوم دیدم و جدی آقا ما رو کجاها برد... چقدر دلم تنگ شده برای اون عصرهایی که از شریف با مترو میومدم انقلاب و از اونجا تا فردوسی رو پیاده میرفتم پایین. یا اون ماهای آخر که با حسین همش کتابخونه دانشگاه تهران پلاس بودیم و ماه رمضونا میرفتیم توی cave ساندویچ میخوردیم.