Διδακτορικές Σπουδές

Λογική και Πληροφορική Ι: Εφαρμογές της Λογικής στον Συναρτησιακό Προγραμματισμό

Περιγραφή

Η Υπολογισιμότητα, και ως προς το τι μπορεί να υπολογιστεί και ως προς το πώς μπορεί αυτό να υπολογιστεί, βρίσκει με εντυπωσιακό τρόπο το ανάλογο της στα πλαίσια της Λογικής. Η έννοια του τυπικού συστήματος, η αναπαραστασιμότητα των αναδρομικών συναρτήσεων, η μορφή των προγραμμάτων κατ' αναλογία με τη μορφή των φυσικών αποδείξεων είναι μερικά από τα σημεία σύνδεσης της Λογικής με την Πληροφορική. Αυτό μας επιτρέπει να χρησιμοποιήσουμε κλασικά αποτελέσματα στη θεωρία της Λογικής και της Θεωρίας Αποδείξεων για τη μελέτη του προγραμματισμού. Ειδικότερα στη Θεωρία του Συναρτησιακού Προγραμματισμού μπορούμε να χρησιμοποιήσουμε το πρωτόκολλο Curry-Howard για τη σχεδίαση συστημάτων με πολυμορφικούς, εξαρτώμενους και επαγωγικούς τύπους με πολλές υλοποιήσεις σε Proof assistants (Coq, Isabelle κ.α.).
Περιεχόμενα: Τυπικά λογικά συστήματα. Η κατασκευαστική Λογική ως πλαίσιο του προγραμματισμού. Προγράμματα με τύπους και τυπικές αποδείξεις, Curry-Howard. Αναδρομικές συναρτήσεις και υπολογισιμότητα. Αναπαραστασιμότητα κλάσεων αναδρομικών συναρτήσεων σε τυπικά συστήματα, Τύποι και τερματισμός προγραμμάτων. Πολυμορφικοί, εξαρτώμενοι, επαγωγικοί τύποι και proof assistants.