a_software.gif
tercer_nivel_software.gif

UPM / IMDEA Software Institute Specialization Track in Software Development through Rigorous Methods (2017-2018)

Note: this course is taught at the the IMDEA Software Institute (in the Montegancedo Campus, 500 m. from the CS School). Please get in touch with the coordinator or one of the instructors for more details regarding the exact meeting place and possible schedule changes.



This course has specific requirements. If you are not a student affiliated to the IMDEA Software Institute, please follow these instructions. If you do not follow them, you may be asked to register in some other course.

Foundations for Programming Languages

Coordinator(s)

Instructor(s)

Length

4 credits (ECTS)

Prerequisites

Course web page (if any)

Not yet available.

Summary and objectives

This course provides the formal background needed to reason about software and programming languages in a precise and mathematically sound way.

Fundamental conceps underlying the design, definition and execution mechanisms of programming languages are covered, including recursion, syntax, various forms of semantics and type systems.

Alongside the theoretical contents, the course may include small programming assignments to gain a more instrumental level of the ideas mentioned above.

Topics

  1. Introduction
    1. Overview, motivation, and challenges for SW technologies
    2. Review of background: programming, logic, mathematical structures…
  2. Syntax
    1. Abstract and concrete syntax definitions
    2. Recursion and induction
  3. Lambda-calculi
    1. Abstract and concrete syntax definitions
    2. The untyped lambda-calculus
    3. Simply-typed lambda-calculus
  4. Semantics
    1. Operational semantics
    2. Denotational semantics
  5. Type systems
    1. Natural deduction
    2. The Curry-Howard isomorphism
    3. Polymorphism
    4. Algebraic/recursive types
    5. Reference types; Monads; Effects
    6. Subtyping

Evaluation

The final grade will be obtained from:

  • A suite of short, individual practical/theoretical exercises periodically proposed which will be worth 50% of the final grade.
  • The remaining 50% will come from from a written exam paper.

Exercises for each unit will have the same relative weight for the overall grade, although individual exercises in a given unit can have different weights.

Recommended reading

Foundations for Programming Languages. John C. Mitchell. The MITPress, 1996.




Back to the initial page
Go to the IMDEA Software Institute page

Fractals are used with permission from their author Cory Ench | © 2006-2007. IMDEA Software.
All rights reserved | Legal Notice | Privacy Policy