CS-452 / 8 crédits

Enseignant: Bourgeat Thomas Emile

Langue: Anglais


Summary

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a program part or a language. Students will learn how to apply these concepts in their reasoning.

Content

- simple types, lambda-calculus

- normalization, references, exceptions

- recursive types

- polymorphism

- proposition as types

- Tentatively: combinatory logic, calculus of inductive constructions

Keywords

lambda-calculus, type systems

Learning Prerequisites

Recommended courses

Advanced topics in programming, Compiler construction

Important concepts to start the course

Functional programming

Basic knowledge of formal languages

Learning Outcomes

By the end of the course, the student must be able to:

  • Argue design decisions of programming languages
  • Assess / Evaluate soundness of type systems
  • Design programming language semantics and typing rules
  • Verify progress and preservation in type systems
  • Work out / Determine operational equivalences
  • Carry out projects of 2-3 weeks duration
  • Distinguish valid from invalid proofs
  • Implement type systems and operational semantics

Transversal skills

  • Assess progress against the plan, and adapt the plan as appropriate.
  • Evaluate one's own performance in the team, receive and respond appropriately to feedback.
  • Identify the different roles that are involved in well-functioning teams and assume different roles, including leadership roles.
  • Manage priorities.

Teaching methods

Ex cathedra, practical exercises

Assessment methods

Final written exam during the exam session (60%)

Projects and homeworks by groups during the semester (40%)

Resources

Moodle Link

Dans les plans d'études

  • Semestre: Printemps
  • Forme de l'examen: Ecrit (session d'été)
  • Matière examinée: Foundations of software
  • Cours: 3 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • Projet: 2 Heure(s) hebdo x 14 semaines
  • Type: optionnel
  • Semestre: Printemps
  • Forme de l'examen: Ecrit (session d'été)
  • Matière examinée: Foundations of software
  • Cours: 3 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • Projet: 2 Heure(s) hebdo x 14 semaines
  • Type: optionnel
  • Semestre: Printemps
  • Forme de l'examen: Ecrit (session d'été)
  • Matière examinée: Foundations of software
  • Cours: 3 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • Projet: 2 Heure(s) hebdo x 14 semaines
  • Type: optionnel
  • Semestre: Printemps
  • Forme de l'examen: Ecrit (session d'été)
  • Matière examinée: Foundations of software
  • Cours: 3 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • Projet: 2 Heure(s) hebdo x 14 semaines
  • Type: optionnel
  • Semestre: Printemps
  • Forme de l'examen: Ecrit (session d'été)
  • Matière examinée: Foundations of software
  • Cours: 3 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • Projet: 2 Heure(s) hebdo x 14 semaines
  • Type: optionnel

Semaine de référence

Lundi, 8h - 11h: Cours ELD020

Mardi, 8h - 10h: Exercice, TP GRB330

Mardi, 10h - 12h: Projet, labo, autre CE1105

Cours connexes

Résultats de graphsearch.epfl.ch.