סילבוס

תוכן הקורס ומטרתו

קורס זה מציג מושגים וטכניקות בסיסיות ביסודות של שפות תכנות, תוך הדגשת הפן הפורמלי שלהם. המוטיב המרכזי בקורס הוא ההסתכלות על תוכנה ושפות תכנות כאובייקטים מתמטיים, אודותיהם ניתן לטעון ולהוכיח טענות מדויקות. הקורס כולו יילמד בעזרת Coq, כלי הוכחה אינטראקטיבי המבוסס על שפת תכנות פונקצינלית עם טיפוסים תלויים. לאחר מבוא לוגי ומבוא לתכנות פונקציונלי, הנושאים שילמדו יכללו: סמנטיקה של שפת תכנות אימפרטיבית פשוטה, מערכות טיפוסים בשפות פונקציונליות פשוטות, פולימורפיזם בתכנות פונקציונלי, לוגיקת Hoare להוכחת נכונות תכניות ועוד.

ידע מוקדם של Coq או של תכנות פונקציונלי אינו נדרש. מאחר ול-Coq עקומת למידה תלולה, הקורס ידרוש השקעה בהיקף משמעותי, ובפרט: שיעורי בית שבועיים ולימוד עצמי של נושאים מסוימים.

הקורס יעקוב ברובו אחר הספר המקוון: https://softwarefoundations.cis.upenn.edu.

הקורס פתוח גם לתלמידי תואר שני ומומלץ למי שמתעניין/עוסק בתאוריה של שפות תכנות, אימות תוכנה ולוגיקה.