Programming languages and compilation - KAIN7M03

  • Number of hours

    • Lectures 15.0
    • Projects -
    • Tutorials 15.0
    • Internship -
    • Laboratory works -
    • Written tests 2.0

    ECTS

    ECTS 0.4

Goal(s)

The objective of this course is twofold.
1) An introduction to the Coq proof assistant, which is authoritative in the field of verification especially for certified compilers and OS.
2) The study of the concepts underlying the compilation of programming languages, in particular the main formalisms used to define their semantics. The practice is based on Coq.

Content(s)

  • Compiler architecture and compilation steps
  • higher-order typed logic, deduction rules
  • structural induction, induction on an inductive relation
  • practice of the Coq proof assistant
  • abstract syntax trees
  • computational and relational semantics of programming languages (functional semantics, natural semantics, structural operational semantics)
  • correct by construction design and implementation of compilers

Prerequisites

Automata and Languages
Knowledge of at least one programming language
Parsing

Test

100% PROJ = project
* Evaluation will be based on the following deliverables:
**# Intermediate session reports (TD)
**# Final projet report (1 for each group)
**# Individual assessment interview

Calendar

The course exists in the following branches:

  • Curriculum - INFO - Semester 7

Additional Information

Course ID : KAIN7M03
Course language(s): FR

You can find this course among all other courses.

Bibliography

  • B. C. Pierce. Types and Programming Languages, MIT press, 2002
  • Software Foundantions, https://softwarefoundations.cis.upenn.edu/index.html
  • A. Aho, R. Sethi, J. Ullman, Compilateurs : Principes, techniques et outils, InterEditions
    - W. Waite and G. Goos, Compiler Construction, Springer Verlag