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

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

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

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

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

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

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

 

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

29/9/2021

Κατά το ακαδημαϊκό έτος 2021-22, το μάθημα δε θα διδαχθεί.

5/10/2020

Κατά το ακαδημαϊκό έτος 2020-21, το μάθημα δε θα διδαχθεί.

23/1/2020

Τα μαθήματα διακόπτονται από τις 30/1, λόγω της εξεταστικής του ΑΛΜΑ. Θα συνεχιστούν από την Πέμπτη 20/2 για λίγες εβδομάδες.

16/1/2020

Την Πέμπτη 30/1 (Τριών Ιεραρχών) θα γίνει η διάλεξη του μαθήματος.

17/10/2019

Οι διαλέξεις θα γίνονται κάθε Πέμπτη, ώρα 10:00–13:00, στο Εργαστήριο Λογισμικού που βρίσκεται στην αίθουσα 1.1.25 του Παλιού Κτιρίου ΗΜΜΥ, ΕΜΠ, στην Πολυτεχνειούπολη Ζωγράφου.

 

Υλικό

Γενικά

   

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

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

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

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

Ασκήσεις

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

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

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

 

Διαλέξεις

Παράδοση 17/10/2019

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

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

Παράδοση 12/12/2019

Παράδοση 19/12/2019

Παράδοση 9/1/2020

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

Παράδοση 23/1/2020

Παράδοση 20/2/2020

 

Τελευταία αλλαγή: 30/10/2019, 18:32 UTC.