دکتری در علوم کامپیوتر بنیادی: دوگانگی خطی و اثرات جبری رده‌بالا در نظریه نوع هموتوپی
چارچوب‌های یکپارچه‌ساز برای منطق خطی، اثرات جبری و نظریه نوع هموتوپی را در دستیاران اثبات بررسی کنید.
مناسب برای:مناسب برای نامزدهای دکتری دارای تخصص در نظریه نوع وابسته، دستیاران اثبات (Agda/Lean/Isabelle) و برنامه‌نویسی تابعی (Haskell/OCaml/Rust).
مرور کلی
این موقعیت دکتری در انستیتو پژوهش در علوم کامپیوتر بنیادی (پاریس) بر توسعه یک چارچوب نحوی و تابعی یکپارچه تمرکز دارد که منطق خطی، اثرات جبری و نظریه نوع هموتوپی را ادغام می‌کند. هدف این پروژه، فرمالیزه کردن و پیاده‌سازی این مفاهیم در دستیاران اثبات مانند Agda، Lean یا Isabelle است تا نسل بعدی دستیاران ریاضی گواهی‌شده به جلو رانده شوند. این کار، مبانی نظری را با کاربردهای عملی در هدایت اثبات خودکار و ساخت سند گواهی‌شده پیوند خواهد داد. متقاضیان باید پیشینه قوی در نظریه نوع وابسته و ابزارهای تأیید صوری، به همراه تسلط بر زبان‌های برنامه‌نویسی تابعی داشته باشند. این موقعیت، یک محیط مشارکتی را در یک مؤسسه پژوهشی پیشرو فرانسوی ارائه می‌دهد.
نحوهٔ درخواست
برای دیدن امتیاز تطابق شخصی، نیازمندی‌ها، جزئیات بودجه و نحوهٔ درخواست — به انگلیسی یا فارسی — حساب کاربری رایگان بساز.