חזרה

סילבוס

מספר קורס 0368-3241-02
שם הקורס יסודות פורמליים של שפות תכנות
יחידה אקדמית הפקולטה למדעים מדויקים ע"ש ריימונד ובברלי סאקלר -
מדעי המחשב
אופן ההוראה תרגיל
שעות סמסטריאליות 1
סמסטר א' תשפ"ב
יום ה
שעות 13:00-14:00
בניין בניין צ'ק פוינט
חדר 001
סאלי ובנימין נמני
אין סילבוס

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

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

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

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



טרם פורסם סילבוס מפורט
מטלות הקורס

ייתכנו מטלות נוספות
רשימת המטלות המלאה תופיע בסילבוס המפורט של הקורס.

קורסי קדם נדרשיםמודלים חישוביים (03682200) +תוכנה 1 (03682157)

דרישות קדם ספציפיות בקורס בהתאם לתוכנית הלימודים הנלמדת,
מופיעות בדף הידיעון של התוכנית



tau logohourglass00:00