Εθνικό Μετσόβιο Πολυτεχνείο
Σχολή Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών
Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών

Συστήματα Τύπων των Γλωσσών Προγραμματισμού

http://courses.softlab.ntua.gr/typesys/

Συστήματα Τύπων των Γλωσσών Προγραμματισμού

Μεταπτυχιακό μάθημα, χειμερινού εξαμήνου
(ΣΗΜΜΥ, κωδικός 631 — ΜΠΛΑ, κωδικός Π03Γ)

Εξάμηνο: Χειμερινό 2011
Διδάσκων:
Νίκος Παπασπύρου   ()   γρ. 1.1.21   τηλ: 210-772-3393

Ανακοινώσεις | Υλικό: Γενικά, Διαφάνειες, Ασκήσεις, Παλαιότερα έτη
Διαλέξεις: 10/11 | 15/11 | 22/11 | 29/11 | 13/12 | 20/12 | 10/1 | 17/1 | 24/1 | 31/1 | 7/2 | 14/2 | 21/2 | 28/2

 

Ανακοινώσεις

13/12/2011

ΠΡΟΣΟΧΗ: Εις το εξής, οι διαλέξεις του μαθήματος θα γίνονται στην Αίθουσα 103, στο Νέο Κτίριο Ηλεκτρολόγων, 1ος όροφος, Πολυτεχνειούπολη Ζωγράφου.

15/11/2011

ΠΡΟΣΟΧΗ: Εις το εξής, οι διαλέξεις του μαθήματος θα γίνονται κάθε Τρίτη, ώρα 15:30–18:30, στο Εργαστήριο Λογισμικού που βρίσκεται στην Αίθουσα 1.1.25, (παλιό) Κτίριο Ηλεκτρολόγων, 1ος όροφος, Πολυτεχνειούπολη Ζωγράφου.

10/11/2011

ΠΡΟΣΟΧΗ: Η δεύτερη διάλεξη του μαθήματος θα γίνει την Τρίτη 15/11, ώρα 15:30–18:30, στο Εργαστήριο Λογισμικού που βρίσκεται στην Αίθουσα 1.1.25, (παλιό) Κτίριο Ηλεκτρολόγων, 1ος όροφος, Πολυτεχνειούπολη Ζωγράφου. Για τις επόμενες διαλέξεις, οι ενδιαφερόμενοι σπουδαστές καλούνται να επιλέξουν μεταξύ δύο εναλλακτικών ημερών και ωρών. (Αν σας κάνουν και οι δύο, δηλώστε και τις δύο.)

 

Υλικό

Γενικά

   

Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002.

Τμήμα του βιβλίου (ps.gz, 460KB) διατίθεται online για εκπαιδευτικό σκοπό μόνο στους σπουδαστές που παρακολουθούν το μάθημα και μόνο μέσω IP διευθύνσεων του ΕΜΠ. Αν παρακολουθείτε το μάθημα και δεν έχετε την δυνατότητα να συνδεθείτε μέσω διεύθυνσης IP του ΕΜΠ, στείλτε e-mail στο διδάσκοντα.

Οι σπουδαστές θα βρουν ιδιαίτερα χρήσιμη την ιστοσελίδα του παραπάνω βιβλίου, την οποία συντηρεί ο συγγραφέας του, και κυρίως τις υλοποιήσεις ελεγκτών τύπων και αποτιμητών για τις γλώσσες που θα μελετηθούν. Για να εκτελέσετε αυτές τις υλοποιήσεις θα χρειαστείτε το μεταγλωττιστή της OCaml, διαθέσιμο από το: http://www.ocaml.org/.

CoqΤο σύστημα υποστήριξης αποδείξεων (proof assistant) Coq είναι διαθέσιμο από το: http://coq.inria.fr/.

Διαφάνειες

Οι παρακάτω διαφάνειες χρησιμοποιήθηκαν στις διαλέξεις εκτός του βιβλίου του Pierce, για συμπληρωματική ύλη. Είναι διαθέσιμες σε δύο μορφές: σε μορφή για παρουσίαση (μία διαφάνεια ανά σελίδα, έγχρωμες, πιθανώς με εφέ κίνησης) και σε μορφή για εκτύπωση (έξι διαφάνειες ανά σελίδα, πιθανώς ασπρόμαυρες).

Ασκήσεις

Οι ασκήσεις θα παραδίδονται στον διδάσκοντα μέσω e-mail σε ηλεκτρονική μορφή (LaTeX). Μπορείτε να παραλείψετε μία σειρά ασκήσεων. Καθυστερημένες ασκήσεις θα βαθμολογούνται με μικρότερο βαθμό, αντιστρόφως ανάλογα προς το χρόνο καθυστέρησης.

Μπορείτε να βασιστείτε σε αυτό το template (TEX, 2ΚΒ). Είναι προσαρμοσμένο για υποστήριξη ελληνικών χαρακτήρων μέσω του XeLaTeX (άλλη εναλλακτική λύση είναι το πακέτο babel). Επίσης, για το typesetting των inference rules ίσως χρειαστεί να εγκαταστήσετε το πακέτο semantic.

Παλαιότερα έτη

 

Διαλέξεις

Παράδοση 10/11/2011

Παράδοση 15/11/2011

Παράδοση 22/11/2011

Παράδοση 29/11/2011

Παράδοση 13/12/2011

Παράδοση 20/12/2011

Παράδοση 10/1/2012

Παράδοση 24/1/2012

Παράδοση 31/1/2012

Παράδοση 14/2/2012

Παράδοση 21/2/2012

Παράδοση 28/2/2012

 

Τελευταία αλλαγή: 29/2/12, 9:34.