Planeamento

Aulas Teóricas

Lecture 01: Introduction to the course

Aula 1

Introduction to the course. General considerations about programming languages. Brief historical remarks about programming languages.

Lecture 02: Basic Functional Programming in Coq

Aula 2

Introduction to Coq.
Functional Programming in Coq: data and functions.

Lecture 03: Working with structured data. Polymorphism.

Aula 3

Working with structured data: pairs, lists, option types.
Polymorphism.

Lecture 04: Polymorphism and Higher-Order Functions

Aula 4

Polymorphic lists. Polymorphic pairs. Implicit arguments.

Functions as Data. Higher-order functions. The function filter.

Lecture 05: Higher-Order Functions and Proving in Coq

Aula 5

Higher-Order Functions: filter, map, and fold. Anonymous functions. Functions as return values and partial application.

Proofs by simplification. Proofs by Rewriting.

Lecture 06: Proving in Coq

Aula 6

Proofs by Rewriting. Proofs by Induction.

Lecture 07: Programming Language Syntax

Aula 7

Regular expressions and context-free grammars as formalisms to describe the syntax of programming languages.
Contextual keywords.
Derivations and parse trees.
Abstract syntax trees (ASTs).
Encoding of ASTs in Coq.

Lecture 08: Abstract Syntax Trees

Aula 8

Abstract Syntax Trees (ASTs)
Encoding and manipulation of ASTs in Coq
Structural induction

Lecture 09: Abstract Syntax Trees, Variables, Bindings, and Scopes

Aula 9

Encoding in Coq of ASTs and variables.
Names and Bindings: binding time, binding lifetime, object lifetime, object storage management
Scopes: static scoping, dynamic scoping

Lecture 10: Semantics via Interpreters

Aula 10

Introduction to formal semantics.

Semantics via interpreters: arithmetic expressions + simple stack machine.
Compiler correctness.

Lecture 11: Semantics via Interpreters (continued)

Aula 11

Semantics via Interpreters: towards imperative languages.
Programs as state transformers. Evaluation.
Algebraic properties of imperative programs.

Lecture 12: Computational vs Relational Evaluation

Aula 12

Computational vs. Relational approaches to evaluation
Inference rules

Lecture 13: Relational Evaluation of Imperative Programs + Intro to Hoare Logic

Aula 13

Relational Evaluation of Imperative Programs
Relational vs Functional Evaluation: advantages / drawbacks
Introduction to Hoare Logic
Assertions, Hoare Triples, and Proof Rules

Lecture 14: Consolidation and Revision

Aula 14

Discussion and solution of the model/previous tests.
Consolidation and revision for the first test.

Lecture 15: Invited Lecture

Aula 15

TBA

Lecture 16: Hoare Logic (continued)

Aula 16

Brief discussion on the solutions to the first test.

Hoare Logic: history and recent developments.
Assertions, triples, proof rules.
Coq Encoding of Assertions and Hoare triples.

Lecture 17: Hoare Logic (continued)

Aula 17

Hoare Logic: Proof rules.
Inference rules and proof trees.
Coq encoding of Proof rules.

Lecture 18: Small-step Semantics

Aula 18

Big-Step vs Small-Step Operational Semantics
Strong Progress and Normal Forms
Small-Step Semantics of a tiny imperative language with concurrency
Encoding in Coq

Lecture 19: Small-step Semantics / Introduction to Types

Aula 19

Small-step semantics (continuation).

Stuck terms.
Types. Typing relations. Type preservation and type soundness.

Lecture 20: Types + Introduction to Lambda Calculus

Aula 20

Types and Typing Relations (continuation).

Introduction to Lambda Calculus.

Lecture 21: Lambda Calculus / Simply Typed Lambda Calculus

Aula 21

Untyped Lambda Calculus: bound variables, free variables, substitution, reduction.

Introduction to the Simply Typed Lambda Calculus.

Lecture 22: Encoding the Simply Typed Lambda Calculus (Part 1)

Aula 22

Encoding in Coq of the Simply Typed Lambda Calculus (Part 1)

Lecture 23: Encoding the Simply Types Lambda Calculus (Part 2, continuation of Lecture 22)

Aula 23

Encoding in Coq of the Simply Typed Lambda Calculus (Part 2, continuation of Lecture 22)

Lecture 24: Typechecking + Subtyping

Aula 24

Exercises on typechecking.
Encoding of a typechecking algorithm. 

Discussion on the soundness and completeness of the typechecking algorithm.
Brief discussion on subtyping.

Lecture 25: Discussion and solutions of the model test. Consolidation.

Aula 25

Discussion and solutions of the model test. Consolidation.

Lecture 26: Project Presentation. Discussion and solutions of the model test. Conclusion.

Aula 26

Students presente their projects.

Further discussion on the solutions of the model test.
Conclusion.

Aulas Laboratoriais

No lab sessions during first week.

Aula 1

No lab sessions during first week.

Practical session 1: Basic Functional Programming in Coq

Aula 2

Functional Programming in Coq: data and functions.

Practical Session 2: Polymorphic lists, Higher-order functions, Basic Proving

Aula 3

Definition of recursive (polymorphic) functions on (polymorphic) lists.
Higher-order functions on lists (map, filter, fold).
Proofs by simplification and rewriting.

Practical Session 3: Polymorphic trees, Maps

Aula 4

Polymorphic trees
Proof by structural induction
Maps (open activity)

Practical Session 4: Abstract Syntax Trees / Syntax

Aula 5

Consolidation of material from previous labs.
Encoding and manipulation of ASTs in Coq.
Syntax.

Practical Session 5: Semantics of a simple imperative language

Aula 6

Semantics of a simple imperative language (using functional evaluation and a restricted form of loops)
Open activity: explore the addition of conventional While loops

Practical Session 6: Relational Evaluation

Aula 7

Implementation of semantics in Coq as a relation.

Practical Session 7: Step-Indexed Evaluation

Aula 8

Implementation of a step-indexed evaluation for an imperative language with unbounded loops.

Practical Session 8: Hoare Logic

Aula 9

Exercises on Hoare Logic

Practical Session 9: Hoare Logic (continuation)

Aula 10

Exercises on Hoare Logic (Part 2)

Practical Session 10: Small-step semantics / Typing rules

Aula 11

Definition and encoding of a small-step semantics for a tiny imperative language.

Definition and encoding of typing rules for a term language. Using the rules to typecheck terms.

Practical Session 11: Lambda Calculus

Aula 12

Exercises on the Untyped Lambda Calculus.

Encoding the Simply Typed Lambda Calculus.

Practical Session 12: Simply Typed Lambda Calculus

Aula 13

Encoding of the Simply Typed Lambda Calculus and some extensions (such as let bindings).