MSE Master of Science in Engineering

The Swiss engineering master's degree

Jedes Modul umfasst 3 ECTS. Sie wählen insgesamt 10 Module/30 ECTS in den folgenden Modulkategorien:

  • ​​​​12-15 ECTS in Technisch-wissenschaftlichen Modulen (TSM)
    TSM-Module vermitteln Ihnen profilspezifische Fachkompetenz und ergänzen die dezentralen Vertiefungsmodule.
  • 9-12 ECTS in Erweiterten theoretischen Grundlagen (FTP)
    FTP-Module behandeln theoretische Grundlagen wie die höhere Mathematik, Physik, Informationstheorie, Chemie usw. Sie erweitern Ihre abstrakte, wissenschaftliche Tiefe und tragen dazu bei, den für die Innovation wichtigen Bogen zwischen Abstraktion und Anwendung spannen zu können.
  • 6-9 ECTS in Kontextmodulen (CM)
    CM-Module vermitteln Ihnen Zusatzkompetenzen aus Bereichen wie Technologiemanagement, Betriebswirtschaft, Kommunikation, Projektmanagement, Patentrecht, Vertragsrecht usw.

In der Modulbeschreibung (siehe: Herunterladen der vollständigen Modulbeschreibung) finden Sie die kompletten Sprachangaben je Modul, unterteilt in die folgenden Kategorien:

  • Unterricht
  • Dokumentation
  • Prüfung
Advanced Programming Paradigms (TSM_AdvPrPa)

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.


Eintrittskompetenzen

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.


Lernziele

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.


Modulinhalt

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

Lehr- und Lernmethoden

Interactive lectures explaining main concepts, interspersed with programming exercises and reading assignments.


Bibliografie

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.

 

Vollständige Modulbeschreibung herunterladen

Zurück