Λέσχη Μαθηματικών
Χειμερινό εξάμηνο 2024-25
|
02 Αίθουσα A31 Ώρα 15:00 |
Μία εισαγωγή στην Agda: Βασικά προγραμματιστικά στοιχεία (Μέρος 1 από τα 2) Αβουκάτος Ανδρέας Περίληψη: Στο πρώτο μέρος ορίζουμε στοιχειώδεις δομές (όπως π.χ. οι φυσικοί αριθμοί), διατυπώνουμε προτάσεις και τις αποδεικνύουμε στο περιβάλλον της Agda. Μέσω της διαδραστικής τυποποίησης γνώριμων δομών και γεγονοτών, θα μάθουμε τη σύνταξη και την ελαφρώς ιδιαίτερη προσέγγιση στον προγραμματισμό που έχει η Agda. Στόχος της παρουσίασης είναι η εξοικείωση με την Agda, ώστε στο δεύτερο μέρος να δούμε μέσω αυτής τη Martin-Löf dependent type theory (η ραχοκοκαλιά της Agda), όπως και πιο ενδιαφέρουσες δομές (higher inductive types), univalence, κ.α. Abstract: In the first part we define elementary structures (such as the natural numbers), formulate propositions and prove them in the Agda environment. Through interactive formalization of familiar structures and events, we will learn the syntax and the slightly special approach to programming that Agda requires. The goal of the first presentation is to familiarize ourselves with Agda, in order to delve into the Martin-Löf dependent type theory (the backbone of Agda), as well as to see more interesting structures (higher inductive types), univalence, etc, in the second part. Προαπαιτούμενες γνώσεις: Καμία Βιβλιογραφία:
|
|---|