Chaque module vaut 3 ECTS. Vous sélectionnez 10 modules/30 ECTS parmi les catégories suivantes:
- 12-15 crédits ECTS en Modules technico-scientifiques (TSM)
Les modules TSM vous transmettent une compétence technique spécifique à votre orientation et complètent les modules de spécialisation décentralisés. - 9-12 crédits ECTS en Bases théoriques élargies (FTP)
Les modules FTP traitent de bases théoriques telles que les mathématiques élevées, la physique, la théorie de l’information, la chimie, etc., vous permettant d’étendre votre profondeur scientifique abstraite et de contribuer à créer le lien important entre l’abstraction et l’application dans le domaine de l’innovation. - 6-9 crédits ECTS en Modules contextuels (CM)
Les modules CM vous transmettent des compétences supplémentaires dans des domaines tels que la gestion des technologies, la gestion d’entreprise, la communication, la gestion de projets, le droit des brevets et des contrats, etc.
Le descriptif de module (download pdf) contient le détail des langues pour chaque module selon les catégories suivantes:
- leçons
- documentation
- examen
Although widespread, the currently mainstream imperative, object-oriented programming paradigm, with testing as its main method of quality assurance, has its limitations. Even though it allows novices to write programs relatively quickly and without much formal training, such programs tend to become complicated as soon as they need to do something non-trivial. This makes them increasingly hard to write and reason about, making assurance methods that give better guarantees than software testing intractable. Similarly, even though it is possible to write software tests relatively quickly and without much formal training, such tests are only able to show the presence of faults, but never their absence.
Few are aware that there exist a number of alternatives to imperative, object-oriented programming and testing. This course will start with a broad overview of these alternatives, and then focus on one of them, functional programming, and the use of formal methods to specify and prove the correctness of functional programs.
Functional programming is an approach to programming where simplicity, clarity, and elegance are the key goals. It is the application of formal mathematical and programming-language-based techniques for the construction and verification of computer programs. Although it has a long history, it has recently received attention due to its potential for writing elegant, correct and efficient programs that are easier to write, compose, and maintain, once one is familiar with its underlying concepts. Its simplicity also allows reasoning about the correctness of functional programs using techniques taught in high-school mathematics. These techniques can not only be used to state and prove functional correctness of smaller programs on paper, but also large systems using automated proof assistants. Such automated proof assistants (e.g. Agda, Isabelle/HOL, Idris, Lean and Coq) are themselves applications and further developments of functional programming.
In the final segment of the course, we broaden our focus to explore sophisticated type systems in imperative, object-oriented and functional programming languages. These advanced type systems serve as effective tools for program verification, and have proven effective for identifying and eliminating critical bugs.
Compétences préalables
All participants should be able to program in the functional and object-oriented styles to the degree that can be expected after attending an introductory-level undergraduate course on these topics.
Participants without prior experience in functional programming are required to work through the chapters 1 through 8 in the book "Programming in Haskell" (second edition) by Graham Hutton before starting the course.
Objectifs d'apprentissage
All participants are able to explain and apply formal programming-language-based techniques for the construction and verification of computer programs. Special emphasis will be made on techniques that surpass some of the limitations of mainstream programming in the imperative object-oriented programming style, and on alternatives to mainstream testing-based software assurance methods.
All participants should be able to:
- enumerate and explain a number of different programming paradigms.
- construct programs in the functional style.
- verify the correctness of functional programs using formal proof.
- apply advanced type systems to make imperative, object-oriented and functional programs more secure.
Contenu des modules
The following is a rough overview of the content of the course and is subject to change:
- Overview (1 week)
- A broad overview of different programming paradigms.
- Functional Programming (4 weeks)
- Fast paced revision of functional programming prerequisites and Haskell.
- Types for correctness, Input/Output in a pure language.
- Functional design patterns: Functor, Applicative and Monad with parsing as an example application.
- Application: Interpreters for a small imperative and functional programming language.
- Proving Programs Correct (5 weeks)
- Equational reasoning
- Structural induction
- Automated theorem proving
- Dependent types
- Advanced Type Systems (4 weeks)
- Subtyping with generic types (co- and contravariance)
- Subtyping lattices
- Ownership typing
- Effect systems
Méthodes d'enseignement et d'apprentissage
Interactive lectures explaining main concepts, interspersed with programming exercises and reading assignments.
Bibliographie
You are required to have a copy of the following book during the course:
- Graham Hutton, Programming in Haskell, Second Edition, Cambridge, 2016.
Further material will be provided during the course as required.
Télécharger le descriptif complet
Retour