Ασφάλεια σε Συστήματα Τύπων με Τύπους Τομής και Άρνησης

Abstract

Ο προγραμματισμός ηλεκτρονικών υπολογιστών είναι αρκετά πιο δημοφιλής σήμερα, με ολοένα και περισσότερα άτομα να ασχολούνται με αυτόν. Γλώσσες προγραμματισμού υψηλού επιπέδου με πανίσχυρες γενικευμένες έννοιες κάνουν εύκολο για τον οποιονδήποτε να γράψει προγράμματα. Από την άλλη μεριά, το να δείξει κανείς ότι ένα πρόγραμμα έχει την επιθυμητή συμπεριφορά είναι μία αρκετά δυσκολότερη διαδικασία. Ο έλεγχος τύπων είναι η πιο βασική προσέγγιση για να το επιτύ- χουμε. Σε αυτήν τη διπλωματική, παρουσιάζουμε ένα στατικό σύστημα τύπων, που περιέχει τύπους τομής και άρνησης και μία σχέση υποτύπων, ώστε να αναθέσουμε αρκετά περιγραφικούς τύπους σε προγράμματα μία απλής συναρτησιακής γλώσσας με ταίριασμα προτύπων. Δείχνουμε ότι το σύστημα τύπων μας αναθέτει τύπους μόνο σε προγράμματα με καθορισμένη σημασιολογία, δηλαδή, ότι έχει την ιδιότητα της ασφάλειας τύπων.