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

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

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

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

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

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

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

 

ΠΡΟΣΟΧΗ! Το μάθημα φέτος περιλαμβάνει δύο εναλλακτικές ενότητες. (Οι σπουδαστές του ΜΠΛΑ επιλέγουν υποχρεωτικά την πρώτη ενότητα.)

Ο ιστότοπος αυτός αναφέρεται σε όσους επιλέξουν την πρώτη ενότητα. Για την εναλλακτική δεύτερη ενότητα, ακολουθήστε τον παραπάνω σύνδεσμο.

 

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

5/11/2008

Οι διαλέξεις του μαθήματος θα γίνονται στο εξής κάθε Παρασκευή, ώρα 10:00–13:00, στο Εργαστήριο Τεχνολογίας Λογισμικού, Αίθουσα 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/.

Ασκήσεις

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

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

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

 

Διαλέξεις

Παράδοση 15/10/2008

Παράδοση 24/10/2008

Παράδοση 31/10/2008

Παράδοση 7/11/2008

Παράδοση 14/11/2008

Παράδοση 21/11/2008

Παράδοση 28/11/2008

Παράδοση 16/1/2009

Παράδοση 6/2/2009

Παράδοση 13/2/2009

 

Τελευταία αλλαγή: 18/2/09, 10:05.