Foundations of software
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%)
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