Σημασιολογία στην Επιστήμη των Υπολογιστών

Περίγραμμα μαθήματος

Εισαγωγή στον λ-λογισμό με τύπους ανώτερης τάξης. Κανόνες αναγραφής λ-όρων. Ελάχιστα σταθερά σημεία και αναδρομή. Η παραδειγματική συναρτησιακή γλώσσα PCF και η αποτίμηση προγραμμάτων PCF. Μοντέλα του λ-λογισμού. Πλήρεις μερικές διατάξεις και συνεχείς συναρτήσεις. Σημασιολογία της γλώσσας PCF. Θεωρήματα πληρότητας για τον λ-λογισμό. Η μέθοδος των λογικών σχέσεων. Ισχυρή κανονικοποίηση και ιδιότητα Church-Rosser του λ- λογισμού. Συσχετισμός αποτίμησης και σημασιολογίας της γλώσσας PCF. Το θεώρημα επάρκειας. Το θεώρημα αφαιρετικότητας για την γλώσσα PCF με παράλληλο έλεγχο. Αναδρομικοί τύποι και προδιαγραφές δομών δεδομένων. Σημασιολογία και θεώρημα επάρκειας για την PCF με αναδρομικούς τύπους. Η μέθοδος των περιεκτικών σχέσεων. Εισαγωγή στη σημασιολογία γλωσσών με πολυμορφικούς τύπους. Εισαγωγή στη σημασιολογία αντικειμενοστραφών γλωσσών.