Please use this identifier to cite or link to this item: http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14428
Title: Αναπτυξη Βιβλιοθηκης Θεωριων Για Την Αποδειξη Ιδιοτητων Πιστοποιημενου Κωδικα.
Authors: Τσοκος Θεοδωρος
Παπασπύρου Νικόλαος
Keywords: συστηματα τυπων
λαμβδα λογισμος
λογισμος των επαγωγικων κατασκευων
προγραμματισμος με αποδειξεις
ασφαλεια εκτελεσιμου κωδικα
γλωσσα τυπων nflint
coq.
Issue Date: 21-Oct-2005
Abstract: Σκοπός αυτής της διπλωματικής εργασίας είναι η μελέτη συστημάτων λάμβδα λογισμού, η αντιστοιχία τους με συστήματα μαθηματικής λογικής, και στη συνέχεια η καταγραφή και απόδειξη χρήσιμων θεωριών σε μια παραλλαγή του λογισμού των επαγωγικών κατασκευών (Calculus of Inductive Constructions --- CIC), τη γλώσσα τύπων nflint. Η βιβλιοθήκη θεωριών που αναπτύχθηκαν μπορούν να ενσωματωθούν στην ήδη υπάρχουσα δουλειά, στην προσπάθεια κατασκευής ενός συστήματος παραγωγής πιστοποιημένου εκτελέσιμου κώδικα.Ο λάμβδα-λογισμός είναι ένα πλήρες υπολογιστικό σύστημα με μεγάλη εκφραστικότητα. Από τις αρχές της δεκαετίας του 1930, όταν Alonso Church όρισε τον κλασσικό λάμβδα-λογισμό χωρίς τύπους, αναπτύχθηκαν πολλές παραλλαγές του με τύπους οι οποίες αντιστοιχούν, μέσω του ισομορφισμού Curry-Howard, σε συστήματα λογικής. Μέσω αυτής της αντιστοίχισης, ο λαμβδα λογισμός αποτελεί λοιπόν βασικό εργαλείο γιατη καταγραφή και την απόδειξη θεωριών.Η δύναμη της εκφραστικότητας της γλώσσας τύπων nflint, σε συνδυασμό με την τυπικότητα και το βάθος του συστήματος λογικής που αντιστοιχεί στο λογισμό των επαγωγικών κατασκευών, αποτελούν σήμερα μία ελπιδοφόρα πρόταση στο ζήτημα της παραγωγής πιστοποιημένου και ασφαλούς εκτελέσιμου κώδικα, ένα ζήτημα που έχει απασχολήσει πολύ τελευταία, ότανμεγάλα συστήματα λογισμικού έδειξαν αδυναμία στην ασφάλεια, προκαλώντας έτσι και οικονομικά προβλήματα. Έτσι, με βάση μία γλώσσα προγραμματισμού με ισχυρό σύστημα τύπων, καταγράφονται και αποδεικνύονται χρήσιμες ιδιότητες του εκτελέσιμου κώδικα, πιστοποιώντας έτσι τη σωστή και ασφαλή λειτουργία του. Σε ένα τέτοιο πλαίσιο πιστοποίησης της ασφάλειας του εκτελέσιμου κώδικα, η γλώσσα τύπων nflint είναι το μέσο για την καταγραφή των τυπικών συλλογισμών. Όμως, απαιτείται ένα σύνολο θεωριών και αποδείξεων της λογικής που θα χρησιμοποιηθούν για την απόδειξη των ιδιοτήτων που θα καταγραφούν με τη χρήση της nflint. Επειδή το σύστημαυποστήριξης αποδείξεων Coq χρησιμοποιεί και αυτό μια παραλλαγή του λογισμού των επαγωγικών κατασκευών και διαθέτει μια πλούσια βιβλιοθήκη θεωριών, κρίθηκε ουσιαστικό και αποτελεσματικό, η ανάπτυξη ενός συνόλου βιβλιοθηκών για τη γλώσσα τύπων να ακολουθήσει τη δομή της βιβλιοθήκης του συστήματος Coq. Έτσι, με ημιαυτόματο τρόπο, αναπτύχθηκε στο πλαίσιο αυτής της διπλωματικής εργασίας ένα σύνολο από θεωρίες και αποδείξεις της λογικής --- βασικοί τύποι, προτασιακή και κατηγορηματική λογική, αριθμητική Peano --- στη γλώσσα τύπων nflint.
URI: http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14428
Appears in Collections:Διπλωματικές Εργασίες - Theses

Files in This Item:
File SizeFormat 
DT2005-0216.pdf720.6 kBAdobe PDFView/Open


Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.