| Entrambe le parti precedenti la revisioneRevisione precedenteProssima revisione | Revisione precedente |
| magistraleinformatica:psc:2020-21:start [05/02/2022 alle 16:52 (3 anni fa)] – [Lectures (2nd part)] Roberto Bruni | magistraleinformatica:psc:2020-21:start [05/02/2022 alle 16:55 (3 anni fa)] (versione attuale) – [Lectures (1st part)] Roberto Bruni |
|---|
| | 7 | Mon | 01/03 | 16:00-18:00 | Teams | 05 - Induction (ctd.):\\ //determinacy of arithmetic expressions, structural induction over many-sorted signatures, termination of boolean expressions, memories, update operation, operational semantics of commands, divergence// | {{ :magistraleinformatica:psc:2021-03-01_-_05b_-_more_induction.pdf |Lecture 05b}} | | | 7 | Mon | 01/03 | 16:00-18:00 | Teams | 05 - Induction (ctd.):\\ //determinacy of arithmetic expressions, structural induction over many-sorted signatures, termination of boolean expressions, memories, update operation, operational semantics of commands, divergence// | {{ :magistraleinformatica:psc:2021-03-01_-_05b_-_more_induction.pdf |Lecture 05b}} | |
| | 8 | Wed | 03/03 | 14:00-16:00 | Teams | 05 - Induction (ctd.):\\ //rule for divergence, limits of structural induction, induction on derivations, rule induction, determinacy of commands// | {{ :magistraleinformatica:psc:2021-03-03_-_05c_-_rule_induction.pdf |Lecture 05c}} | | | 8 | Wed | 03/03 | 14:00-16:00 | Teams | 05 - Induction (ctd.):\\ //rule for divergence, limits of structural induction, induction on derivations, rule induction, determinacy of commands// | {{ :magistraleinformatica:psc:2021-03-03_-_05c_-_rule_induction.pdf |Lecture 05c}} | |
| | 9 | Fri | 05/03 | 14:00-16:00 | Teams | Exercises:\\ //induction, termination, determinacy, divergence//\\ \\ 06 - Equivalence:\\ //operational equivalence, concrete equivalences, parametric equivalences, equivalence and divergence// | {{ :magistraleinformatica:psc:2021-03-05_-_exercises_02.pdf |Exercises 02}}\\ \\ {{ :magistraleinformatica:psc:2021-03-05_-_06_-_equivalence.pdf |Lecture 06}} | | | 9 | Fri | 05/03 | 14:00-16:00 | Teams | Exercises:\\ //induction, termination, determinacy, divergence//\\ \\ 06 - Equivalence:\\ //operational equivalence, concrete equivalences, parametric equivalences, equivalence and divergence// | {{ :magistraleinformatica:psc:2020-21:02_-_properties.pdf |Exercises 02}}\\ \\ {{ :magistraleinformatica:psc:2021-03-05_-_06_-_equivalence.pdf |Lecture 06}} | |
| | 10 | Mon | 08/03 | 16:00-18:00 | Teams | 07 - Induction and recursion:\\ //well-founded recursion, denotational semantics of arithmetic expressions, consistency of operational and denotational semantics for arithmetic expressions, lexicographic precedence relation, Ackermann function, fixpoint equations// | {{ :magistraleinformatica:psc:2021-03-08_-_07_-_recursion.pdf |Lecture 07}} | | | 10 | Mon | 08/03 | 16:00-18:00 | Teams | 07 - Induction and recursion:\\ //well-founded recursion, denotational semantics of arithmetic expressions, consistency of operational and denotational semantics for arithmetic expressions, lexicographic precedence relation, Ackermann function, fixpoint equations// | {{ :magistraleinformatica:psc:2021-03-08_-_07_-_recursion.pdf |Lecture 07}} | |
| | 11 | Wed | 10/03 | 14:00-16:00 | Teams | Exercises:\\ //x++, arithmetic expressions with side-effects//\\ \\ 08 - Partial orders and fixpoints:\\ //partial orders, Hasse diagrams, chains, least element, minimal element, bottom element, upper bounds, least upper bound, chains, limits, complete partial orders, powerset completeness// | {{ :magistraleinformatica:psc:2021-03-10_-_08a_-_cpo.pdf |Lecture 08a}} | | | 11 | Wed | 10/03 | 14:00-16:00 | Teams | Exercises:\\ //x++, arithmetic expressions with side-effects//\\ \\ 08 - Partial orders and fixpoints:\\ //partial orders, Hasse diagrams, chains, least element, minimal element, bottom element, upper bounds, least upper bound, chains, limits, complete partial orders, powerset completeness// | {{ :magistraleinformatica:psc:2021-03-10_-_08a_-_cpo.pdf |Lecture 08a}} | |
| | 12 | Fri | 12/03 | 14:00-16:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //prefix independence, CPO of partial functions, monotonicity, continuity, Kleene's fixpoint theorem// | {{ :magistraleinformatica:psc:2021-03-12_-_08b_-_kleene.pdf |Lecture 08b}} | | | 12 | Fri | 12/03 | 14:00-16:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //prefix independence, CPO of partial functions, monotonicity, continuity, Kleene's fixpoint theorem// | {{ :magistraleinformatica:psc:2021-03-12_-_08b_-_kleene.pdf |Lecture 08b}} | |
| | 13 | Mon | 15/03 | 16:00-18:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //recursive definitions of partial functions as logical systems, immediate consequences operator, set of theorems as fixpoint//\\ \\ 09 - Denotational semantics:\\ //lambda-notation, free variables, capture-avoiding substitutions, alpha-conversion, beta rule, conditionals// | {{ :magistraleinformatica:psc:2021-03-15_-_08c_-_ico.pdf |Lecture 08c}}\\ \\ {{ :magistraleinformatica:psc:2021-03-15_-_09_-_denotational_imp.pdf |Lecture 09}} | | | 13 | Mon | 15/03 | 16:00-18:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //recursive definitions of partial functions as logical systems, immediate consequences operator, set of theorems as fixpoint//\\ \\ 09 - Denotational semantics:\\ //lambda-notation, free variables, capture-avoiding substitutions, alpha-conversion, beta rule, conditionals// | {{ :magistraleinformatica:psc:2021-03-15_-_08c_-_ico.pdf |Lecture 08c}}\\ \\ {{ :magistraleinformatica:psc:2021-03-15_-_09_-_denotational_imp.pdf |Lecture 09}} | |
| | 14 | Wed | 17/03 | 14:00-16:00 | Teams | 09 - Denotational semantics (ctd.):\\ //denotational semantics of commands, fixpoint computation//\\ \\ 10 - Consistency:\\ //denotational equivalence, congruence, compositionality principle, consistency of commands, correctness, completeness//\\ \\ Exercises:\\ //well-founded recursion, posets, semantics// | {{ :magistraleinformatica:psc:2021-03-17_-_10_-_consistency_imp.pdf |Lecture 10}}\\ \\ {{ :magistraleinformatica:psc:2021-03-17_-_exercises_03.pdf |Exercises 03}} | | | 14 | Wed | 17/03 | 14:00-16:00 | Teams | 09 - Denotational semantics (ctd.):\\ //denotational semantics of commands, fixpoint computation//\\ \\ 10 - Consistency:\\ //denotational equivalence, congruence, compositionality principle, consistency of commands, correctness, completeness//\\ \\ Exercises:\\ //well-founded recursion, posets, semantics// | {{ :magistraleinformatica:psc:2021-03-17_-_10_-_consistency_imp.pdf |Lecture 10}}\\ \\ {{ :magistraleinformatica:psc:2020-21:03_-_poset.pdf |Exercises 03}} | |
| | 15 | Fri | 19/03 | 14:00-16:00 | Teams | 10 - Consistency (ctd.):\\ //completeness//\\ \\ Exercises:\\ //well-founded recursion, rule induction//\\ \\ 11 - Haskell:\\ //an overview// | {{ :magistraleinformatica:psc:2021-03-19_-_11_-_haskell.pdf |Lecture 11}} | | | 15 | Fri | 19/03 | 14:00-16:00 | Teams | 10 - Consistency (ctd.):\\ //completeness//\\ \\ Exercises:\\ //well-founded recursion, rule induction//\\ \\ 11 - Haskell:\\ //an overview// | {{ :magistraleinformatica:psc:2021-03-19_-_11_-_haskell.pdf |Lecture 11}} | |
| | 16 | Mon | 22/03 | 16:00-18:00 | Teams | Haskell ghci:\\ //basics, lambda, tuples, lists, list comprehension, guards, pattern matching, partial application, recursive definitions, zip, exercises//\\ {{ :magistraleinformatica:psc:ghci-session1-2021.txt.zip |ghci session 01}} | [[https://www.haskell.org/|Haskell]] | | | 16 | Mon | 22/03 | 16:00-18:00 | Teams | Haskell ghci:\\ //basics, lambda, tuples, lists, list comprehension, guards, pattern matching, partial application, recursive definitions, zip, exercises//\\ {{ :magistraleinformatica:psc:ghci-session1-2021.txt.zip |ghci session 01}} | [[https://www.haskell.org/|Haskell]] | |
| | 17 | Wed | 24/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //costrutto let-in, costrutto where, map, filter, fixpoint operator, exercises//\\ {{ :magistraleinformatica:psc:ghci-session2-2021.txt.zip |ghci session 02}} | [[https://www.haskell.org/|Haskell]] | | | 17 | Wed | 24/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //costrutto let-in, costrutto where, map, filter, fixpoint operator, exercises//\\ {{ :magistraleinformatica:psc:ghci-session2-2021.txt.zip |ghci session 02}} | [[https://www.haskell.org/|Haskell]] | |
| | 18 | Fri | 26/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //tail recursion, folds, application, function composition, data types, type classes, recursive data structures, derived instances, exercises//\\ {{ :magistraleinformatica:psc:ghci-session3-2021.txt.zip |ghci session 03}} | [[https://www.haskell.org/|Haskell]] | | | 18 | Fri | 26/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //tail recursion, folds, application, function composition, data types, type classes, recursive data structures, derived instances, exercises//\\ {{ :magistraleinformatica:psc:ghci-session3-2021.txt.zip |ghci session 03}} | [[https://www.haskell.org/|Haskell]] | |
| | 19 | Mon | 29/03 | 16:00-18:00 | Teams | Exercises:\\ //Haskell//\\ \\ 12 - HOFL:\\ //syntax, type system, type checking// | {{ :magistraleinformatica:psc:2021-03-29_-_12a_-_hofl_types.pdf |Lecture 12a}} | | | 19 | Mon | 29/03 | 16:00-18:00 | Teams | Exercises:\\ //Haskell//\\ \\ 12 - HOFL:\\ //syntax, type system, type checking// | {{ :magistraleinformatica:psc:2020-21:04_-_haskell.pdf |Exercises 04}}\\ {{ :magistraleinformatica:psc:2021-03-29_-_12a_-_hofl_types.pdf |Lecture 12a}} | |
| | 20 | Wed | 31/03 | 14:00-16:00 | Teams | 12 - HOFL (ctd.):\\ //type inference, principal type, canonical forms, operational semantics, lazy vs eager evaluation// | {{ :magistraleinformatica:psc:2020-21:04_-_haskell.pdf |Exercises 04}}\\ {{ :magistraleinformatica:psc:2021-03-31_-_12b_-_hofl_operational.pdf |Lecture 12b}} | | | 20 | Wed | 31/03 | 14:00-16:00 | Teams | 12 - HOFL (ctd.):\\ //type inference, principal type, canonical forms, operational semantics, lazy vs eager evaluation// | {{ :magistraleinformatica:psc:2021-03-31_-_12b_-_hofl_operational.pdf |Lecture 12b}} | |
| |
| |
