Εθνικό Μετσόβιο Πολυτεχνείο Σχολή Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών Συστήματα Τύπων των Γλωσσών Προγραμματισμού https://courses.softlab.ntua.gr/typesys/

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

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

Ανακοινώσεις | Υλικό: Γενικά, Διαφάνειες, Ασκήσεις, Παλαιότερα έτη
Διαλέξεις: 23/10 | 27/10 | 3/11 | 10/11 | 24/11 | 1/12 | 8/12 | 15/12 | 22/12 | 12/1 | 19/1 | 26/1 | 2/2 | 9/2

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

Υλικό

Γενικά

• Οι διαλέξεις και η διδακτέα ύλη θα ακολουθούν το βιβλίο:

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

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

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

Διαφάνειες

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

• Εξαρτώμενοι τύποι (dependent types)
  Μορφή για παρουσίαση (PDF, 552KB) και για εκτύπωση (PDF, 387KB).

Ασκήσεις

• 1η σειρά ασκήσεων, 15/11, παράδοση 1/12, εκφώνηση (PDF, 76ΚΒ).
• 2η σειρά ασκήσεων, 15/11, παράδοση 8/12, εκφώνηση (PDF, 87ΚΒ).
• 3η σειρά ασκήσεων, 14/12, παράδοση 23/12, εκφώνηση (PDF, 74ΚΒ).
• 4η σειρά ασκήσεων, 2/2, παράδοση 23/2, εκφώνηση (PDF, 83ΚΒ).
• 5η σειρά ασκήσεων, 2/2, παράδοση 8/3, εκφώνηση (PDF, 77ΚΒ).
• 6η σειρά ασκήσεων, 2/2, παράδοση 22/3, εκφώνηση (PDF, 91ΚΒ).

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

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

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

• Σελίδα του μαθήματος για το χειμερινό εξάμηνο: 2013-14, 2012-13, 2011-12, 2010-11, 2009-10, 2008-09, 2007-08, 2006-07, 2005-06.
• Σελίδα του μαθήματος για το εαρινό εξάμηνο: 2003-04.

Διαλέξεις

Παράδοση 23/10/2014

• Διαδικαστικά θέματα
• Εισαγωγή (κεφ. 1, 2)
• Αριθμητική και λογικές τιμές (κεφ. 3)
  • ακέραιοι αριθμοί
  • λογικές τιμές

Παράδοση 27/10/2014

• Αριθμητική και λογικές τιμές (κεφ. 3, 4, συνέχεια)
• Το σύστημα υποστήριξης αποδείξεων Coq
  • Μεταφορά βασικών ορισμών και θεωρημάτων του κεφ. 3 (7 KB)
• Λάμβδα λογισμός χωρίς τύπους (κεφ. 5)
• Αναπαράσταση λ-όρων χωρίς ονόματα μεταβλητών (κεφ. 6)
• Υλοποίηση (κεφ. 7), προαιρετική μελέτη

Παράδοση 3/11/2014

• Αριθμητικές εκφράσεις με τύπους (κεφ. 8)
• Μεταφορά σε Coq: βασικοί ορισμοί και θεωρήματα του κεφ. 8 (5 KB)
• Λάμβδα λογισμός με απλούς τύπους (κεφ. 9)
• Υλοποίηση (κεφ. 10), προαιρετική μελέτη

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

• Κανονικοποίηση (κεφ. 12)
• Απλές επεκτάσεις (κεφ. 11)
  • Τύπος Unit και ακολουθιακή εκτέλεση
  • Επισημείωση (ascription) τύπων
  • Δομή let
  • Ζεύγη, πλειάδες και records
  • Αθροίσματα και variants
  • Αναδρομή
  • Λίστες

Παράδοση 24/11/2014

• Αναφορές (κεφ. 13)
• Εξαιρέσεις (κεφ. 14)

Παράδοση 1/12/2014

• Υποτύποι (κεφ. 15)
• Υποτύποι (κεφ. 16)
• Υλοποίηση (κεφ. 17), προαιρετική μελέτη

Παράδοση 8/12/2014

• Προστακτικά αντικείμενα (κεφ. 18)
• Featherweight Java (κεφ. 19)

Παράδοση 15/12/2014

• Αναδρομικοί τύποι (κεφ. 20, 21)

Παράδοση 22/12/2014

• Ανακατασκευή τύπων (κεφ. 22)

Παράδοση 12/1/2015

• Καθολικοί τύποι (universal types) και παραμετρικός πολυμορφισμός (κεφ. 23)

Παράδοση 19/1/2015

• Υπαρξιακοί τύποι (κεφ. 24)
• Υλοποίηση (κεφ. 25), προαιρετική μελέτη

Παράδοση 26/1/2015

• Φραγμένη ποσοτικοποίηση (κεφ. 26, κεφ. 28)
• Προστακτικά αντικείμενα, ξανά (κεφ. 27)

Παράδοση 2/2/2015

• Κατασκευαστές τύπων και είδη (κεφ. 29)
• Τύποι υψηλής τάξης (κεφ. 30)
• Υποτύποι υψηλής τάξης (κεφ. 31)

Παράδοση 9/2/2015

• Καθαρά συναρτησιακά αντικείμενα (κεφ. 32)
• Εξαρτώμενοι τύποι (βλ. σχετικές διαφάνειες)
• Το σύστημα υποστήριξης αποδείξεων Coq, προαιρετική μελέτη
  • Απλές αποδείξεις στον προτασιακό λογισμό (1 KB)
  • Απόδειξη: η τετραγωνική ρίζα του 2 είναι άρρητος αριθμός (3 KB)
  • Άλλα παραδείγματα παλιότερων ετών:
    • Παράδειγμα: ιδιότητες φυσικών αριθμών με church numerals (3 KB)
    • Παράδειγμα: ιδιότητες φυσικών αριθμών με επαγωγικούς τύπους (4 KB)
    • Βασικοί ορισμοί και θεωρήματα του κεφ. 3 (7 KB)
    • Βασικοί ορισμοί και θεωρήματα του κεφ. 8 (5 KB)
  • Περισσότερες πληροφορίες