Αναπτυξη Βιβλιοθηκης Θεωριων Για Την Αποδειξη Ιδιοτητων Πιστοποιημενου Κωδικα.

Abstract

Σκοπός αυτής της διπλωματικής εργασίας είναι η μελέτη συστημάτων λάμβδα λογισμού, η αντιστοιχία τους με συστήματα μαθηματικής λογικής, και στη συνέχεια η καταγραφή και απόδειξη χρήσιμων θεωριών σε μια παραλλαγή του λογισμού των επαγωγικών κατασκευών (Calculus of Inductive Constructions --- CIC), τη γλώσσα τύπων nflint. Η βιβλιοθήκη θεωριών που αναπτύχθηκαν μπορούν να ενσωματωθούν στην ήδη υπάρχουσα δουλειά, στην προσπάθεια κατασκευής ενός συστήματος παραγωγής πιστοποιημένου εκτελέσιμου κώδικα.Ο λάμβδα-λογισμός είναι ένα πλήρες υπολογιστικό σύστημα με μεγάλη εκφραστικότητα. Από τις αρχές της δεκαετίας του 1930, όταν Alonso Church όρισε τον κλασσικό λάμβδα-λογισμό χωρίς τύπους, αναπτύχθηκαν πολλές παραλλαγές του με τύπους οι οποίες αντιστοιχούν, μέσω του ισομορφισμού Curry-Howard, σε συστήματα λογικής. Μέσω αυτής της αντιστοίχισης, ο λαμβδα λογισμός αποτελεί λοιπόν βασικό εργαλείο γιατη καταγραφή και την απόδειξη θεωριών.Η δύναμη της εκφραστικότητας της γλώσσας τύπων nflint, σε συνδυασμό με την τυπικότητα και το βάθος του συστήματος λογικής που αντιστοιχεί στο λογισμό των επαγωγικών κατασκευών, αποτελούν σήμερα μία ελπιδοφόρα πρόταση στο ζήτημα της παραγωγής πιστοποιημένου και ασφαλούς εκτελέσιμου κώδικα, ένα ζήτημα που έχει απασχολήσει πολύ τελευταία, ότανμεγάλα συστήματα λογισμικού έδειξαν αδυναμία στην ασφάλεια, προκαλώντας έτσι και οικονομικά προβλήματα. Έτσι, με βάση μία γλώσσα προγραμματισμού με ισχυρό σύστημα τύπων, καταγράφονται και αποδεικνύονται χρήσιμες ιδιότητες του εκτελέσιμου κώδικα, πιστοποιώντας έτσι τη σωστή και ασφαλή λειτουργία του. Σε ένα τέτοιο πλαίσιο πιστοποίησης της ασφάλειας του εκτελέσιμου κώδικα, η γλώσσα τύπων nflint είναι το μέσο για την καταγραφή των τυπικών συλλογισμών. Όμως, απαιτείται ένα σύνολο θεωριών και αποδείξεων της λογικής που θα χρησιμοποιηθούν για την απόδειξη των ιδιοτήτων που θα καταγραφούν με τη χρήση της nflint. Επειδή το σύστημαυποστήριξης αποδείξεων Coq χρησιμοποιεί και αυτό μια παραλλαγή του λογισμού των επαγωγικών κατασκευών και διαθέτει μια πλούσια βιβλιοθήκη θεωριών, κρίθηκε ουσιαστικό και αποτελεσματικό, η ανάπτυξη ενός συνόλου βιβλιοθηκών για τη γλώσσα τύπων να ακολουθήσει τη δομή της βιβλιοθήκης του συστήματος Coq. Έτσι, με ημιαυτόματο τρόπο, αναπτύχθηκε στο πλαίσιο αυτής της διπλωματικής εργασίας ένα σύνολο από θεωρίες και αποδείξεις της λογικής --- βασικοί τύποι, προτασιακή και κατηγορηματική λογική, αριθμητική Peano --- στη γλώσσα τύπων nflint.