Corsi Anno Accademico 2022/2023


The course aims to introduce formal computer science methods using tools based on type theory, especially AGDA. Lectures will concern the grounds of type theory, namely intuitionistic logic and lambda calculus, eventually focussing on dependent types and Martin-Loef intuitionistic type theory, of which AGDA is an implementation.

See https://dott-informatica.campusnet.unito.it/do/corsi.pl/Show?_id=gu2e

The course is composed by a standard part and a customized part.

Standard part:

  • model of tasks, machines, and schedulers
  • real-time constraints
  • popular scheduling algorithms and tests for real-time tasks on a single processor
  • popular scheduling algorithms and tests for real-time tasks on a multi processor
  • virtual processors

The customized part will be decided in agreement with the participating students. It may include selected topics among:

  • Linux
    • the scheduler, setting the desired scheduler
    • tracing events
  • KVM
    • virtualization with KVM
  • Communication along task chains
  • basics of Zephyr RTOS