Αναδρομικοί Τύποι Στον Προγραμματισμό Με Αποδείξεις

Abstract

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