Please use this identifier to cite or link to this item: http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14166
Full metadata record
DC FieldValueLanguage
dc.contributor.authorΜιχάλης Παπακυριάκου
dc.date.accessioned2018-07-23T14:29:27Z-
dc.date.available2018-07-23T14:29:27Z-
dc.date.issued2004-10-22
dc.date.submitted2004-12-22
dc.identifier.urihttp://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14166-
dc.description.abstractΣκοπός της εργασίας είναι η υλοποίηση ενός ελεγκτή τύπων (typechecker) και ενός διερμηνέα (interpreter) για μια γλώσσα τύπων, βασισμένη στο λογισμό των επαγωγικών κατασκευών (Calculus of Inductive Constructions-CIC). Η γλώσσα αυτή είναι αρκετά εκφραστική ώστε να μπορεί ναχρησιμοποιηθεί για την κωδικοποίηση της κατηγορηματικής λογικής υψηλής τάξης. Η υλοποίησή μας μπορεί αφενός να χρησιμεύσει στο πλαίσιο ενός αυτόματου ή ημιαυτόματου συστήματος αποδείξεων θεωρημάτων. Αφετέρου,μπορεί να ενσωματωθεί στο σύστημα τύπων μιας γλώσσας προγραμματισμού ώστε η τελευταία να υποστηρίζει την παραγωγή πιστοποιημένου εκτελέσιμου κώδικα.Η ανάγκη για αξιόπιστο και πιστοποιημένα ασφαλή εκτελέσιμο κώδικα είναι ακόμα μεγαλύτερη σήμερα, από ό,τι στο παρελθόν. Σε πολυάριθμες περιπτώσεις, προβλήματα ασφάλειας και συμβατότητας προγραμμάτων που έγιναν γνωστά, είχαν ως αποτέλεσμα να θέσουν σε κίνδυνο στην λειτουργία μεγάλων συστημάτων και συνεπώς οικονομικές επιπτώσεις στους οργανισμούς που τα χρησιμοποιούσαν. Για την παραγωγή πιστοποιημένου κώδικα μία τεχνική που κερδίζει έδαφος τα τελευταία χρόνια είναι η πιστοποίηση μέσω ισχυρών συστημάτων τύπων που ενσωματώνουν κατάλληλα συστήματα λογικής, μέσω των οποίων διατυπώνονται και αποδεινύονται προτάσεις ασφαλείας.Σε ένα τέτοιο σύστημα πιστοποίησης της ασφάλειας εκτελέσιμου κώδικα, η γλώσσα των τύπων που είναι το θέμα αυτής της εργασίας αποτελεί το τμήμα της γλώσσας προγραμματισμού στο οποίο γίνονται όλοι οι τυπικοί συλλογισμοί. Μια παραλλαγή αυτής της γλώσσας έχει υλοποιηθεί στο εργαλείο υποστήριξης αποδείξεων Coq. Σε ένα πολύγλωσσο προγραμματιστικό περιβάλλον, η γλώσσα των τύπων θα αποτελεί τον κοινό παρονομαστή όλων των γλωσσών προγραμματισμού που μπορούν να χρησιμοποιηθούν για την υλοποίηση συστημάτων. Όμως, η γλώσσα τύπων που υλοποιείται στην παρούσα εργασία είναι χρήσιμη και αυτοτελώς, στο πλαίσιο ενός συστήματος κωδικοποίησης θεωριών και αποδείξεως θεωρημάτων βασισμένου την κατηγορηματική λογική υψηλής τάξης.Η υλοποίηση της γλώσσας τύπων βασίστηκε σε τεχνικές που βελτιστοποιούν την απόδοση, όπως ο κατακερματισμός (hash-consing), η κωδικοποίηση με ανώνυμες μεταβλητές μέσω των δεικτών de-Bruijn και η χρήση της ασθενούς κανονικής μορφής κεφαλής (weak head normal form) για την βελτίωση τηςαπόδοσης του ελέγχου τύπων. Με κριτήριο την απόδοση και τηνλειτουργικότητα που προσφέρει επιλέχθηκε επίσης η γλώσσα υλοποίησης. Χρησιμοποιήθηκε η OCaml, μία γλώσσα που αναπτύχθηκε με τέτοιου είδους χαρακτηριστικά ώστε να προσφέρεται για την ανάπτυξη τέτοιων εφαρμογών. Από τα αποτελέσματα που παρατηρήθηκαν, ελέγχθηκε η ορθότητα καιμετρήθηκε η απόδοση της παρούσας υλοποίησης της γλώσσας τύπων.
dc.languageGreek
dc.subjectσυστήματα τύπων
dc.subjectλογισμός των επαγωγικών κατασκευών
dc.subjectπρογραμματισμός με αποδείξεις
dc.subjectασφάλεια εκτελέσιμου κώδικα
dc.subjectocaml
dc.titleΥλοποίηση Μιας Γλώσσας Τύπων Με Εφαρμογές Στην Πιστοποίηση Εκτελέσιμου Κώδικα
dc.typeDiploma Thesis
dc.description.pages75
dc.contributor.supervisorΠαπασπύρου Νικόλαος
dc.departmentΤομέας Τεχνολογίας Πληροφορικής & Υπολογιστών
dc.organizationΕΜΠ, Τμήμα Ηλεκτρολόγων Μηχανικών & Μηχανικών Υπολογιστών
Appears in Collections:Διπλωματικές Εργασίες - Theses

Files in This Item:
File SizeFormat 
DT2004-0210.pdf796.07 kBAdobe PDFView/Open


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