Ο φοιτητής του προγράμματος Βάιος-Ραφαήλ Μιχαλάκης θα παρουσιάσει τη διπλωματική του εργασία με θέμα:
Data-types as Objects Revisited: Insights and Proofs
την Τετάρτη 18 Δεκεμβρίου 2024 και ώρα 18:00, μέσω τηλεμετάδοσης (google meet).
Σύνοψη Διπλωματικής:
Η παρούσα διατριβή ασχολείται με μια προσέγγιση για την απόδοση της σημασιολογίας των τύπων δεδομένων σε απλές γλώσσες συναρτησιακού προγραμματισμού. Η περιεχόμενη ύλη είναι μια λεπτομερώς επαναδιατυπωμένη έκδοση του [SW77] που συμπληρώνεται με αποδείξεις και ιδέες, οι οποίες απουσίαζαν σε μεγάλο βαθμό από την αρχική εργασία. Η προσέγγιση του [SW77] έχει επηρεάσει αρκετές μεταγενέστερες εργασίες και αποτέλεσε τη βάση για την ανάπτυξη του λεγόμενου μοντέλου ιδεωδών για αναδρομικούς πολυμορφικούς τύπους. Η κύρια ιδέα της προαναφερθείσας δημοσίευσης είναι να αντιμετωπίζονται οι τύποι δεδομένων ως αντικείμενα της γλώσσας προγραμματισμού— για να γίνει αυτό, οι συγγραφείς ανέπτυξαν ένα τυπικό σύστημα στο οποίο μπορούν να γίνουν ουσιαστικοί υπολογισμοί με τύπους δεδομένων, συμπεριλαμβανομένου του αναδρομικού ορισμού των τύπων δεδομένων ή της εφαρμογής τους σε συναρτήσεις: υπό το πρίσμα του ισομορφισμού Curry-Howard, αυτό σημαίνει ότι μπορεί κανείς να χρησιμοποιήσει στην πραγματικότητα τον υπολογισμό με τύπους δεδομένων για να αποδείξει ιδιότητες των προγραμμάτων. Το μοντέλο που προκύπτει επιτρέπει την ύπαρξη υποτύπων και υπερτύπων, καθώς και λογικώς προσδιορισμένων τύπων και μιας περιορισμένης μορφής οικογενειών εξαρτημένων τύπων, έννοιες που είναι πολύ δυσκολότερο να οριστούν στα παραδοσιακά συστήματα τύπων. Στη διατριβή διερευνούμε τους τυπικούς ορισμούς των σχετικών εννοιών και παρουσιάζουμε (με πλήρεις αποδείξεις) τις βασικές ιδιότητές τους, τόσο σε αφηρημένο επίπεδο, όσο και σε αυτό των εφαρμογών στον έλεγχο τύπου πραγματικών προγραμμάτων. Προς καλύτερη κατανόηση του τελευταίου από τον αναγνώστη, ανάμεσα στη συλλογή των θεωρημάτων και των περιγραφόμενων τεχνικών υπάρχουν διάσπαρτα μερικά διαφωτιστικά παραδείγματα, που δείχνουν την ευελιξία και τη δύναμη της θεωρίας που εξετάζεται.
Η Επιτροπή,
Νικόλαος Ρήγας,
Εξωτερικός συνεργάτης
Παναγιώτης Ροντογιάννης (Συνεπιβλέπων),
Τμήμα Πληροφορικής, Ε.Κ.Π.Α.
Άγγελος Χαραλαμπίδης (Συνεπιβλέπων),
Τμήμα πληροφορικής, Χαροκόπειο Πανεπιστήμιο
William Wadge,
University of Victoria