| Entrambe le parti precedenti la revisioneRevisione precedenteProssima revisione | Revisione precedente |
| magistraleinformatica:psc:start [24/02/2025 alle 13:21 (2 settimane fa)] – [Lectures (1st part)] Roberto Bruni | magistraleinformatica:psc:start [08/03/2025 alle 17:01 (5 giorni fa)] (versione attuale) – [Lectures (1st part)] Roberto Bruni |
|---|
| ==== Announcements ==== | ==== Announcements ==== |
| | |
| | * The lectures of **thursday Feb 27 and friday Feb 28 are canceled** due to conflicting events, |
| * as the course starts:\\ Each student must subscribe the [[https://teams.microsoft.com/l/team/19%3AcpAGDU3sLif2Mzf3MqTStZSPslNMJlv74wBG859yE7Y1%40thread.tacv2/conversations?groupId=eb61dc9a-ff03-4418-877d-2ad467640293&tenantId=c7456b31-a220-47f5-be52-473828670aa1|Microsoft Teams channel]] of the course and then fill the form [[https://forms.office.com/e/p8RwTeLvMd|Students information]] to provide the following contact data and info about her/his background: | * as the course starts:\\ Each student must subscribe the [[https://teams.microsoft.com/l/team/19%3AcpAGDU3sLif2Mzf3MqTStZSPslNMJlv74wBG859yE7Y1%40thread.tacv2/conversations?groupId=eb61dc9a-ff03-4418-877d-2ad467640293&tenantId=c7456b31-a220-47f5-be52-473828670aa1|Microsoft Teams channel]] of the course and then fill the form [[https://forms.office.com/e/p8RwTeLvMd|Students information]] to provide the following contact data and info about her/his background: |
| - **first name** | - **first name** |
| | 2 | Thu | 20/02 | 14:00-16:00 | C1 | 02 - Preliminaries (ctd):\\ //denotational semantics, compositionality principle, normalisation, determinacy, consistency, equivalence, congruence//\\ \\ 03 - Unification:\\ //inference process, signatures, substitutions, most general than relation, unification problem// | {{ :magistraleinformatica:psc:2025-02-18_-_02_-_semantics.pdf |Lecture 02}}\\ {{ :magistraleinformatica:psc:2025-02-20_-_03_-_unification.pdf |Lecture 03}} | | | 2 | Thu | 20/02 | 14:00-16:00 | C1 | 02 - Preliminaries (ctd):\\ //denotational semantics, compositionality principle, normalisation, determinacy, consistency, equivalence, congruence//\\ \\ 03 - Unification:\\ //inference process, signatures, substitutions, most general than relation, unification problem// | {{ :magistraleinformatica:psc:2025-02-18_-_02_-_semantics.pdf |Lecture 02}}\\ {{ :magistraleinformatica:psc:2025-02-20_-_03_-_unification.pdf |Lecture 03}} | |
| | 3 | Fri | 21/02 | 09:00-11:00 | L1 | 03 - Unification (ctd):\\ //unification problem, most general unifiers, unification algorithm//\\ \\ 04 - Logical systems:\\ //logical systems, derivations, theorems, logic programs, goal-oriented derivations// | {{ :magistraleinformatica:psc:2025-02-20_-_03_-_unification.pdf |Lecture 03}}\\ {{ :magistraleinformatica:psc:2025-02-21_-_04_-_logic.pdf |Lecture 04}} | | | 3 | Fri | 21/02 | 09:00-11:00 | L1 | 03 - Unification (ctd):\\ //unification problem, most general unifiers, unification algorithm//\\ \\ 04 - Logical systems:\\ //logical systems, derivations, theorems, logic programs, goal-oriented derivations// | {{ :magistraleinformatica:psc:2025-02-20_-_03_-_unification.pdf |Lecture 03}}\\ {{ :magistraleinformatica:psc:2025-02-21_-_04_-_logic.pdf |Lecture 04}} | |
| | 4 | | | | | Exercises:\\ //unification, goal-oriented derivations//\\ \\ 05 - Induction:\\ //precedence relation, infinite descending chains, well-founded relations, well-founded induction, mathematical induction, proof of induction principle, structural induction, termination of arithmetic expressions, determinacy of arithmetic expressions// | Exercises 01\\ Lecture 05a\\ Lecture 05b | | | 4 | Tue | 25/02 | 16:00-18:00 | A1 | Exercises:\\ //unification, goal-oriented derivations//\\ \\ 05 - Induction:\\ //precedence relation, infinite descending chains, well-founded relations, well-founded induction, mathematical induction, proof of induction principle, structural induction, termination of arithmetic expressions// | {{ :magistraleinformatica:psc:01_-_inference_-_2025.pdf |Exercises 01}}\\ {{ :magistraleinformatica:psc:2025-02-24_-_05a_-_induction.pdf |Lecture 05a}} | |
| | 5 | | | | | Exercises:\\ //induction//\\ \\ 05 - Induction (ctd.):\\ //many-sorted signatures, arithmetic and boolean expressions, structural induction over many-sorted signatures, termination of boolean expressions, memories, update operation, operational semantics of commands// | Lecture 05b | | | - | Thu | 27/02 | 14:00-16:00 | C1 | **Canceled due to travelling constraints** | | |
| | 6 | | | | | 05 - Induction (ctd.):\\ //divergence, rule for divergence, limits of structural induction, induction on derivations, rule induction, determinacy of commands// | Lecture 05c | | | - | Fri | 28/02 | 09:00-11:00 | L1 | **Canceled due to graduation event** | | |
| | 7 | | | | | 06 - Equivalence:\\ //operational equivalence, concrete equivalences, parametric equivalences, equivalence and divergence//\\ \\ 07 - Induction and recursion:\\ //well-founded recursion, lexicographic precedence relation, Ackermann function, denotational semantics of arithmetic expressions, fixpoint equations// | Lecture 06\\ Lecture 07 | | | 5 | Tue | 04/03 | 16:00-18:00 | A1 | Exercises:\\ //induction//\\ \\ 05 - Induction (ctd.):\\ //determinacy of arithmetic expressions, many-sorted signatures, arithmetic and boolean expressions, structural induction over many-sorted signatures, termination of boolean expressions, memories, update operation, operational semantics of commands// | {{ :magistraleinformatica:psc:2025-03-04_-_05b_-_more_induction.pdf |Lecture 05b}} | |
| | 8 | | | | | 07 - Induction and recursion (ctd):\\ //consistency of operational and denotational semantics for arithmetic expressions//\\ \\ 08 - Partial orders and fixpoints (ctd.):\\ //partial orders, Hasse diagrams, chains, least element, minimal element, bottom element, upper bounds, least upper bound, limits, complete partial orders, powerset completeness, prefix independence, CPO of partial functions, monotonicity// | Lecture 07\\ Lecture 08a\\ Lecture 08b | | | 6 | Thu | 06/03 | 14:00-16:00 | C1 | 05 - Induction (ctd.):\\ //divergence, rule for divergence, limits of structural induction, induction on derivations, rule induction, determinacy of commands// | {{ :magistraleinformatica:psc:2025-03-06_-_05c_-_rule_induction.pdf |Lecture 05c}} | |
| | 9 | | | | | Exercises:\\ //induction, termination, determinacy, divergence//\\ \\ 08 - Partial orders and fixpoints (ctd.):\\ //continuity, Kleene's fixpoint theorem, McCarthy's 91 function// | Exercises 02\\ Lecture 08b\\ | | | 7 | Fri | 07/03 | 09:00-11:00 | L1 | 06 - Equivalence:\\ //operational equivalence, concrete equivalences, parametric equivalences, equivalence and divergence//\\ \\ 07 - Induction and recursion:\\ //well-founded recursion, lexicographic precedence relation, Ackermann function, denotational semantics of arithmetic expressions, consistency of operational and denotational semantics for arithmetic expressions, fixpoint equations// | {{ :magistraleinformatica:psc:2025-03-07_-_06_-_equivalence.pdf |Lecture 06}}\\ {{ :magistraleinformatica:psc:2025-03-07_-_07_-_recursion.pdf |Lecture 07}} | |
| | 10 | | | | | Exercises:\\ //well-founded recursion, posets, semantics//\\ \\ 08 - Partial orders and fixpoints (ctd.):\\ //recursive definitions of partial functions as logical systems, immediate consequences operator, set of theorems as fixpoint// | Exercises 03\\ Lecture 08c | | | 8 | Tue | 11/03 | 09:00-11:00 | E | 08 - Partial orders and fixpoints (ctd.):\\ //partial orders, Hasse diagrams, chains, least element, minimal element, bottom element, upper bounds, least upper bound, limits, complete partial orders, powerset completeness, prefix independence, CPO of partial functions, monotonicity// | Lecture 08a\\ Lecture 08b | |
| | | 9 | Thu | 13/03 | 14:00-16:00 | C1 | Exercises:\\ //induction, termination, determinacy, divergence//\\ \\ 08 - Partial orders and fixpoints (ctd.):\\ //continuity, Kleene's fixpoint theorem, McCarthy's 91 function// | Exercises 02\\ Lecture 08b\\ | |
| | | 10 | Fri | 14/03 | 09:00-11:00 | L1 | Exercises:\\ //well-founded recursion, posets, semantics//\\ \\ 08 - Partial orders and fixpoints (ctd.):\\ //recursive definitions of partial functions as logical systems, immediate consequences operator, set of theorems as fixpoint// | Exercises 03\\ Lecture 08c | |
| | 11 | | | | | 09 - Denotational semantics:\\ //lambda-notation, free variables, capture-avoiding substitutions, alpha-conversion, beta rule, conditionals, denotational semantics of commands, fixpoint computation//\\ \\ 10 - Consistency:\\ //denotational equivalence, congruence, compositionality principle, consistency of commands, correctness, completeness// | Lecture 09\\ Lecture 10 | | | 11 | | | | | 09 - Denotational semantics:\\ //lambda-notation, free variables, capture-avoiding substitutions, alpha-conversion, beta rule, conditionals, denotational semantics of commands, fixpoint computation//\\ \\ 10 - Consistency:\\ //denotational equivalence, congruence, compositionality principle, consistency of commands, correctness, completeness// | Lecture 09\\ Lecture 10 | |
| | 12 | | | | | 11 - Haskell:\\ //an overview//\\ \\ Haskell ghci:\\ //basics, tuples, lists, list comprehension, guards, pattern matching, lambda, partial application, zip, exercises// | [[https://www.haskell.org/|Haskell]]\\ Lecture 11\\ ghci session 01 | | | 12 | | | | | 11 - Haskell:\\ //an overview//\\ \\ Haskell ghci:\\ //basics, tuples, lists, list comprehension, guards, pattern matching, lambda, partial application, zip, exercises// | [[https://www.haskell.org/|Haskell]]\\ Lecture 11\\ ghci session 01 | |
