Συστήματα Τύπων των Γλωσσών Προγραμματισμού
Μεταπτυχιακό μάθημα, χειμερινού εξαμήνου
Εξάμηνο: Χειμερινό 2007
Διδάσκων:
Νίκος Παπασπύρου
(nickie (AT) softlab (DOT) ntua.gr )
γρ. 1.1.21
τηλ: 210-772-3393
Ανακοινώσεις | Υλικό:
Γενικά , Διαφάνειες , Παλαιότερα έτη Διαλέξεις: 22/11 |
29/11 | 6/12 |
13/12 | 20/12 | 10/1 | 17/1 | 24/1 |7/2 | 11/2 | 21/2
30/10/2007 Οι διαλέξεις του μαθήματος θα γίνονται στο εξής κάθε Πέμπτη , ώρα 10:00–13:00 , στο Εργαστήριο Τεχνολογίας Λογισμικού, Αίθουσα 1.1.25, Κτίριο Ηλεκτρολόγων, 1ος όροφος, Πολυτεχνειούπολη Ζωγράφου.
Υλικό
Οι διαλέξεις και η διδακτέα ύλη θα ακολουθούν το βιβλίο:
Benjamin C. Pierce , Types and Programming Languages , MIT Press, 2002.
Τμήμα του βιβλίου (ps.gz , 460KB) διατίθεται online για εκπαιδευτικό σκοπό μόνο στους σπουδαστές του ΕΜΠ που παρακολουθούν το μάθημα και μόνο μέσω IP διευθύνσεων του ΕΜΠ .
ιστοσελίδα του παραπάνω βιβλίου , την οποία συντηρεί ο συγγραφέας του, και κυρίως τις υλοποιήσεις ελεγκτών τύπων και αποτιμητών για τις γλώσσες που θα μελετηθούν. Για να εκτελέσετε αυτές τις υλοποιήσεις θα χρειαστείτε το μεταγλωττιστή της OCaml, διαθέσιμο από το: http://www.ocaml.org/ .
Οι παρακάτω διαφάνειες χρησιμοποιήθηκαν στις διαλέξεις εκτός του βιβλίου του Pierce, για συμπληρωματική ύλη. Είναι διαθέσιμες σε δύο μορφές: σε μορφή για παρουσίαση (μία διαφάνεια ανά σελίδα, έγχρωμες, πιθανώς με εφέ κίνησης) και σε μορφή για εκτύπωση (έξι διαφάνειες ανά σελίδα, πιθανώς ασπρόμαυρες).
Διαλέξεις
Εισαγωγή (κεφ. 1, 2)
συστήματα τύπων
δομημένη λειτουργική σημασιολογία
Αριθμητική και λογικές τιμές (κεφ. 3, 4)
ακέραιοι αριθμοί
λογικές τιμές
Λάμβδα λογισμός χωρίς τύπους (κεφ. 5)
Αναπαράσταση λ-όρων χωρίς ονόματα μεταβλητών (κεφ. 6)
Υλοποίηση (κεφ. 7), προαιρετική μελέτη
Παρουσίαση: Νίκος Παπασπύρου
Αριθμητικές εκφράσεις με τύπους (κεφ. 8)
Λάμβδα λογισμός με απλούς τύπους (κεφ. 9)
Υλοποίηση (κεφ. 10), προαιρετική μελέτη
Κανονικοποίηση (κεφ. 12)
Απλές επεκτάσεις (κεφ. 11)
Τύπος Unit και ακολουθιακή εκτέλεση
Επισημείωση (ascription) τύπων
Δομή let
Ζεύγη, πλειάδες και records
Παρουσίαση: Νίκος Παπασπύρου
Απλές επεκτάσεις (κεφ. 11)
Αθροίσματα και variants
Αναδρομή
Λίστες
Αναφορές (κεφ. 13)
Εξαιρέσεις (κεφ. 14)
Παρουσίαση: Πάνος Προκοπίου
Υποτύποι (κεφ. 15, κεφ. 16)
Υλοποίηση (κεφ. 17), προαιρετική μελέτη
Παρουσίαση: Νίκος Παπασπύρου , Μιχάλης Παπακυριάκου
Προστακτικά αντικείμενα (κεφ. 18)
Featherweight Java (κεφ. 19)
Παρουσίαση: Χάρης Νάκος
Αναδρομικοί τύποι (κεφ. 20, κεφ. 21)
Παρουσίαση: Γιώργος Πιερράκος
Ανακατασκευή τύπων (κεφ. 22)
Καθολικοί τύποι (universal types) και παραμετρικός πολυμορφισμός (κεφ. 23)
Υλοποίηση (κεφ. 25), προαιρετική μελέτη
Παρουσίαση: Θάνος Τσουάνας
Υπαρξιακοί τύποι (κεφ. 24)
Φραγμένη ποσοτικοποίηση (κεφ. 26, κεφ. 28)
Παρουσίαση: Χάρης Νάκος
Προστακτικά αντικείμενα, ξανά (κεφ. 27)
Κατασκευαστές τύπων και είδη (κεφ. 29)
Τύποι υψηλής τάξης (κεφ. 30)
Παρουσίαση: Πάνος Προκοπίου
Υποτύποι υψηλής τάξης (κεφ. 31)
Καθαρά συναρτησιακά αντικείμενα (κεφ. 32)
Παρουσίαση: Γιώργος Πιερράκος
Εξαρτώμενοι τύποι (βλ. σχετικές διαφάνειες )
Ισομορφισμός Curry-Howard
Το σύστημα υποστήριξης αποδείξεων Coq
Παρουσίαση: Νίκος Παπασπύρου
Τελευταία αλλαγή: 24/2/08, 15:45.
webmaster (AT) courses (DOT) softlab.ntua.gr
Οι σπουδαστές θα βρουν ιδιαίτερα χρήσιμη την ιστοσελίδα του παραπάνω βιβλίου, την οποία συντηρεί ο συγγραφέας του, και κυρίως τις υλοποιήσεις ελεγκτών τύπων και αποτιμητών για τις γλώσσες που θα μελετηθούν. Για να εκτελέσετε αυτές τις υλοποιήσεις θα χρειαστείτε το μεταγλωττιστή της OCaml, διαθέσιμο από το: http://www.ocaml.org/.