Eπαληθευμένες βελτιστοποιήσεις για συναρτησιακές γλώσσες

Περίληψη

Το σύστημα Coq είναι ένα από τα πιο διαδεδομένα συστήματα μηχανικών αποδείξεων. Επιτρέπει στους χρήστες να γράφουν συναρτησιακά προγράμματα, να εκφράζουν τυπικές προδιαγραφές για αυτά, και στη συνέχεια να τις αποδεικνύουν μέσω μιας διαλογικής διεπαφής. Τα προγράμματα που είναι γραμμένα σε Coq μπορούν να εξαχθούν σε μία από τις γλώσσες OCaml, Haskell, ή Scheme και στην συνέχεια να μεταγλωττιστούν και να εκτελεστούν. Όταν το πρόγραμμα Coq συνοδεύεται από μια μηχανική απόδειξη ορθότητας, τότε το πρόγραμμα που εξάγεται πρόκειται για ένα πιστοποιημένο πρόγραμμα. Ωστόσο, σφάλματα τόσο στο πρόγραμμα εξαγωγής όσο και στους μεταγλωττιστές μπορούν να δημιουργήσουν σημασιολογικές διαφορές μεταξύτου τελικού εκτελέσιμου και του αρχικού προγράμματος, με αποτέλεσμα οι αποδεδειγμένες ιδιότητες να μην ισχύουν για τον τελικό κώδικα. Προκειμένου να επιτευχθεί πιστοποίηση του προγράμματος απο άκρη σε άκρη, χρειάζεται ο τελικός κώδικας να παράγεται μέσω μιας πιστοποιημένης διαδικασίας μεταγλώττισης. Επιπλέ ...
περισσότερα

Περίληψη σε άλλη γλώσσα

Coq is one of the most widely adopted proof development systems. It allows programmers to write purely functional programs and verify them against specifications with machine-checked proofs. After verification, one can use Coq's extraction plugin to obtain a program (in OCaml, Haskell, or Scheme) that can be compiled and executed. However, bugs in either the extraction function or the compiler of the extraction language can render source-level verification useless. A verified compiler is a compiler whose output provably preserves thesemantics of the source language. CertiCoq is a verified compiler, currently under development, for Coq's specification language, Gallina. CertiCoq targets Clight, a subset of the C language, that can be compiled with the CompCert verified compiler to obtain a certified executable, bridging the gap between the formally verified source program and the compiled target program. In this thesis, I present the implementation and verification of CertiCoq's optimiz ...
περισσότερα

Όλα τα τεκμήρια στο ΕΑΔΔ προστατεύονται από πνευματικά δικαιώματα.

DOI
10.12681/eadd/55614
Διεύθυνση Handle
http://hdl.handle.net/10442/hedi/55614
ND
55614
Εναλλακτικός τίτλος
Verified optimizations for functional languages
Συγγραφέας
Παρασκευοπούλου, Ζωή (Πατρώνυμο: Αριστομένης)
Ημερομηνία
2020
Ίδρυμα
Princeton University. Department of Computer Science
Εξεταστική επιτροπή
Appel Andrew
Ahmed Amal
Walker David
Gupta Aarti
Kincaid Zachary
Επιστημονικό πεδίο
Φυσικές ΕπιστήμεςΕπιστήμη Ηλεκτρονικών Υπολογιστών και Πληροφορική ➨ Επιστήμη ηλεκτρονικών υπολογιστών, θεωρία και μέθοδοι
Λέξεις-κλειδιά
Ορθότητα μεταγλωττιστών; Συναρτησιακές γλώσσες; Μηχανικές αποδείξεις
Χώρα
Η.Π.Α.
Γλώσσα
Αγγλικά
Άλλα στοιχεία
πιν., σχημ.
Στατιστικά χρήσης
ΠΡΟΒΟΛΕΣ
Αφορά στις μοναδικές επισκέψεις της διδακτορικής διατριβής για την χρονική περίοδο 07/2018 - 07/2023.
Πηγή: Google Analytics.
ΞΕΦΥΛΛΙΣΜΑΤΑ
Αφορά στο άνοιγμα του online αναγνώστη για την χρονική περίοδο 07/2018 - 07/2023.
Πηγή: Google Analytics.
ΜΕΤΑΦΟΡΤΩΣΕΙΣ
Αφορά στο σύνολο των μεταφορτώσων του αρχείου της διδακτορικής διατριβής.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.
ΧΡΗΣΤΕΣ
Αφορά στους συνδεδεμένους στο σύστημα χρήστες οι οποίοι έχουν αλληλεπιδράσει με τη διδακτορική διατριβή. Ως επί το πλείστον, αφορά τις μεταφορτώσεις.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.