ΑΠΟΔΕΙΞΕΙΣ KAI ΠΡΟΓΡΑΜΜΑΤΑ
ο ισομορφισμός Curry-Howard
Μεταπτυχιακό μάθημα (Λ04Α, Λογική και Πληροφορική Ι)
Χειμερινό Εξάμηνο 2004-2005
-
Το μάθημα δίνεται στα πλαίσια του Διαπανεπιστημιακού Μεταπτυχιακού Προγράμματος
στη Λογική και Θεωρία Αλγορίθμων και Υπολογισμού (ΜΠΛΑ) και του Μεταπτυχιακού Προγράμματος (στη Λογική και Πληροφορική) της Σχολής Hλεκτρολόγων Mηχανικών και Mηχανικών Yπολογιστών (ΣHMMY) του ΕΜΠ.
-
Περιγραφή μαθήματος: Ο ισομορφισμός Curry-Howard καθιερώνει μια εκπληκτική απεικόνιση-αναλογία μεταξύ των συστημάτων της τυπικής λογικής, όπως συναντώνται στη θεωρία αποδείξεων (Αποδείξεις) και των συστημάτων υπολογισμού της θεωρίας τύπων (Προγράμματα).
Έτσι με εντυπωσιακό τρόπο συνδέονται δύο (φαινομενικά ξένες) περιοχές, η λογική (θεωρία αποδείξεων) και η πληροφορική (θεωρία τύπων) και ανοίγει ο δρόμος για μια συνεκτική θεωρητική προσέγγιση του μοντέρνου συναρτησιακού προγραμματισμού.
Το μάθημα αποτελεί μια εισαγωγή σε όλες τις πλευρές της θεωρίας τύπων και θεωρίας αποδείξεων που σχετίζονται με τον ισομορφισμό Curry-Howard.
-
Διδάσκοντες: Κολέτσος Γιώργος & Σταυρινός Γιώργος
Περιεχόμενα
-
Εισαγωγή στον λ-λογισμό χωρίς τύπους.
-
Ιντουϊσιονιστική λογική.
-
λ-λογισμός με απλούς τύπους.
-
Εισαγωγή στον ισομορφισμό Curry-Howard.
-
Αποδείξεις ως συνδυαστές.
-
Ελεγχος τυποποίησης.
-
Λογισμός ακολουθητών.
-
Κλασική λογική και τελεστές ελέγχου.
-
Πρωτοβάθμια λογική.
-
Εξαρτώμενοι τύποι.
-
Πρωτοβάθμια αριθμητική και το σύστημα τύπων του Goedel.
-
Δευτεροβάθμια λογική και πολυμορφισμός.
Ωράριο, Πληροφορίες
Θα γίνονται δύο διαλέξεις των δύο ωρών κάθε εβδομάδα:
Δευτέρα 12:30-14:30, αίθ. Α203, κτήριο Α, Γεν. Εδρες, ΕΜΠ
Τετάρτη 12:00-14:00, αίθ. 1.1.29, κτήριο Ηλεκτρολόγων, ΕΜΠ
Συνολική διάρκεια περίπου 12 εβδομάδες. Εναρξη του μαθήματος: Δευτέρα 11 Οκτωβρίου 2004
Πληροφορίες:
Κολέτσος Γιώργος, e-mail: koletsos AT math DOT ntua DOT gr
Σταυρινός Γιώργος, e-mail:
g.stavrinos AT math DOT ntua DOT gr
και στην ιστοσελίδα: http://www.math.ntua.gr/logic/proofgrams
Αναφορές
-
Proofs and Types, J.-Y. Girard, Cambridge Univ. Press, 1989. (URL)
-
Basic Proof theory, A.S. Troelstra & H. Schwichtenberg, 2nd edition,
Cambridge Univ. Press, 2000.
-
Lambda Calculi with Types, H. Barendregt, στο Handbook of Logic in Computer Science, vol. 2, Oxford Univ. Press, 1992. (URL)
-
Basic Simple Type Theory, J.R. Hindley, Cambridge Tracts in Theoretical Computer Science 42, 1996.
-
Proof Theory and Automated Deduction, Jean Goubault-Larrecq & Ian Mackie,
Kluwer Ac. Publ., 1997.
-
Lectures on the Curry-Howard isomorphism, Morten Heine B. Sorensen & Pawel Urzyczyn, 1999.
(URL)
- Intuitionistic Logic, Joan R. Moschovakis, Stanford Encyclopedia of Philosophy, 2004.
(URL)