סילבוס

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

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

ידע מוקדם של Coq או של תכנות פונקציונלי אינו נדרש.
הקורס יעקוב ברובו אחר הספר המקוון: https://softwarefoundations.cis.upenn.edu.

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