| Entrambe le parti precedenti la revisioneRevisione precedente | |
| magistraleinformatica:mpp:start [19/09/2025 alle 09:00 (7 ore fa)] – [Lectures (1st part)] Roberto Bruni | magistraleinformatica:mpp:start [19/09/2025 alle 09:01 (7 ore fa)] (versione attuale) – [Lectures (1st part)] Roberto Bruni |
|---|
| | 1 | Tue | 16/09 | 16:00-18:00 | C1 | 01 - Introduction to the course | | | | 1 | Tue | 16/09 | 16:00-18:00 | C1 | 01 - Introduction to the course | | |
| | 2 | Thu | 18/09 | 09:00-11:00 | L1 | 02 - Preliminaries:\\ //from syntax to semantics, the role of formal semantics, SOS approach, small-step operational semantics, big-step operational semantics, denotational semantics, compositionality principle, normalisation, determinacy, consistency, equivalence, congruence// | | | | 2 | Thu | 18/09 | 09:00-11:00 | L1 | 02 - Preliminaries:\\ //from syntax to semantics, the role of formal semantics, SOS approach, small-step operational semantics, big-step operational semantics, denotational semantics, compositionality principle, normalisation, determinacy, consistency, equivalence, congruence// | | |
| | 3 | Fri | 19/09 | 16:00-18:00 | L1 | 03 - Unification:\\ //inference process, signatures, substitutions, most general than relation, unification problem, most general unifiers, unification algorithm//\\ \\ 04 - Logical systems:\\ //logical systems, derivations, theorems, logic programs, goal-oriented derivations// | | | | 3 | Fri | 19/09 | 16:00-18:00 | L1 | Exercises\\ \\ 03 - Unification:\\ //inference process, signatures, substitutions, most general than relation, unification problem, most general unifiers, unification algorithm//\\ \\ 04 - Logical systems:\\ //logical systems, derivations, theorems, logic programs, goal-oriented derivations// | | |
| | 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// | | | | 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// | | |
| | 5 | | | | | 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// | | | | 5 | | | | | 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// | | |
