Η διάλεξη της Πέμπτης 21/1 δε θα γίνει, γιατί ο διδάσκων θα λείπει στο εξωτερικό.
17/12/2009
Η πρώτη διάλεξη της νέας χρονιάς θα γίνει την Πέμπτη 14/1.
12/10/2009
ΠΡΟΣΟΧΗ: Η πρώτη διάλεξη
του μαθήματος θα γίνει την Πέμπτη 15/10, ώρα 10:00–13:00, στο Εργαστήριο Λογισμικού που
βρίσκεται στην Αίθουσα 1.1.25, (παλιό) Κτίριο Ηλεκτρολόγων, 1ος όροφος, Πολυτεχνειούπολη Ζωγράφου.
Υλικό
Γενικά
Οι διαλέξεις και η διδακτέα ύλη θα ακολουθούν το βιβλίο:
Τμήμα του βιβλίου (ps.gz, 460KB) διατίθεται online για εκπαιδευτικό σκοπό μόνο στους σπουδαστές που παρακολουθούν το μάθημα και μόνο μέσω IP διευθύνσεων του ΕΜΠ. Αν παρακολουθείτε το μάθημα και δεν έχετε την δυνατότητα να συνδεθείτε μέσω διεύθυνσης IP του ΕΜΠ, στείλτε e-mail στο διδάσκοντα.
Το σύστημα υποστήριξης αποδείξεων (proof assistant) Coq είναι διαθέσιμο από το: http://coq.inria.fr/.
Διαφάνειες
Οι παρακάτω διαφάνειες χρησιμοποιήθηκαν στις διαλέξεις εκτός του βιβλίου του Pierce, για συμπληρωματική ύλη. Είναι διαθέσιμες σε δύο μορφές: σε μορφή για παρουσίαση (μία διαφάνεια ανά σελίδα, έγχρωμες, πιθανώς με εφέ κίνησης) και σε μορφή για εκτύπωση (έξι διαφάνειες ανά σελίδα, πιθανώς ασπρόμαυρες).
1η σειρά ασκήσεων, 29/10, παράδοση 15/11, εκφώνηση (PDF, 102ΚΒ).
2η σειρά ασκήσεων, 19/11, παράδοση 3/12, εκφώνηση (PDF, 131ΚΒ).
3η σειρά ασκήσεων, 4/12, παράδοση 20/12, εκφώνηση (PDF, 107ΚΒ).
4η σειρά ασκήσεων, 27/12, παράδοση 14/1, εκφώνηση (PDF, 121ΚΒ).
5η σειρά ασκήσεων, 16/1, παράδοση 31/1, εκφώνηση (PDF, 101ΚΒ).
5η σειρά ασκήσεων, 22/2, παράδοση 10/3, εκφώνηση (PDF, 138ΚΒ).
Οι ασκήσεις θα παραδίδονται στον διδάσκοντα μέσω e-mail σε ηλεκτρονική μορφή (LaTeX).
Μπορείτε να παραλείψετε μία σειρά ασκήσεων. Καθυστερημένες ασκήσεις θα βαθμολογούνται
με μικρότερο βαθμό, αντιστρόφως ανάλογα προς το χρόνο καθυστέρησης.
Μπορείτε να βασιστείτε σε αυτό το template (TEX, 1ΚΒ). Θα χρειαστεί να το προσαρμόσετε στην έκδοση του LaTeX που χρησιμοποιείτε, ανάλογα με την υποστήριξη που διαθέτει για ελληνικά (επικρατέστερες εναλλακτικές λύσεις είναι babel ή XeTeX). Επίσης, για το typesetting των inference rules ίσως χρειαστεί να εγκαταστήσετε το πακέτο semantic.
Οι σπουδαστές θα βρουν ιδιαίτερα χρήσιμη την ιστοσελίδα του παραπάνω βιβλίου, την οποία συντηρεί ο συγγραφέας του, και κυρίως τις υλοποιήσεις ελεγκτών τύπων και αποτιμητών για τις γλώσσες που θα μελετηθούν. Για να εκτελέσετε αυτές τις υλοποιήσεις θα χρειαστείτε το μεταγλωττιστή της OCaml, διαθέσιμο από το: http://www.ocaml.org/.
Το σύστημα υποστήριξης αποδείξεων (proof assistant) Coq είναι διαθέσιμο από το: http://coq.inria.fr/.