Proofs, types, programs, and the Curry–Howard isomorphism
Theoretical and practical course
Topics: | Functional programming, lambda calculus, type theory, proof theory, the Curry–Howard isomorphism. |
---|---|
Prerequisites: | FMC2/FMC3 |
Bibliography: |
|
(In reverse order, because why not…)
Some ideas for projects with students of IMD. Interested students, should contact me ASAP!
Mini-courses I have already offered are available on my teaching website. The following are proposals to consider, in case there is interest.
Students interested in enrolling in these (or related!) courses should contact me by email ASAP!
These could be either optional courses in the following semesters, or “projetos de extensão” that could begin at any convenient time.
The level of each course will depend on (the level of) the interested students.
Theoretical and practical course
Topics: | Functional programming, lambda calculus, type theory, proof theory, the Curry–Howard isomorphism. |
---|---|
Prerequisites: | FMC2/FMC3 |
Bibliography: |
|
Theoretical course
Topics: | Denotational semantics of imperative, functional, and logic programming languages. Model-theoretic, domain-theoretic, and game semantics. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Practical (and a bit theoretical) course
Topics: | Concepts of functional programming, data types, recursion, higher order programming, purely functional programs, lazy evaluation, I/O, type classes, monads, parallel and concurrent programming; dependend types… |
---|---|
Prerequisites: | None |
Bibliography: |
|
Possible projects: | Develop a web application like SIGAA; extend xmonad; clone xmonad; implement a simple programming language. |
Theoretical and practical course
Topics: | Introduction to λProlog and proof search. |
---|---|
Prerequisites: | FMC3, some experience (theoretical or practical) with logic programming |
Bibliography: |
|
Theoretical and practical course
Topics: | Untyped systems, Simple types, Subtyping, Recursive Types, Polymorphism. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Possible projects: | Implement and extend some of Pierce's systems in Haskell, Agda, or Idris. |
Theoretical (and a bit practical) course
Topics: | Lambda calculus, combinatory logic, computable functions, Extensionality, typing à la Church and à la Curry, intersection types, models of λ-calculus, System F. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical course
Topics: | Axiomatic set theory, ZFC, Choice, Ordinals, Cardinals, Independence proofs. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical course
Topics: | Categories, Diagrams, Functors, Natural transformations, Cartesian closed categories, Limits/Colimits. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical course
Topics: | Posets, Lattices, Distributive lattices, Complete lattices, CPOs, Domains, fixpoint theorems. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical (and a bit practical) course
Topics: | Models of computation, Church–Turing thesis, turing machines, finite-state machines, formal languages, grammars, context-free languages, λ-calculus, combinatory logic, primitive recursion, recursive functions, recursive and recursively enumerable sets, s-m-n theorem, the halting problem & unsolvable problems, the arithmetic hierarchy. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical course
Topics: | Propositional and Predicate calculus, Completeness, Incompleteness. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical course
Topics: | Posets, lattices, frames, Heyting algebras, topology, continuity, Scott topology, compactness, locales, Domain theory. |
---|---|
Prerequisites: | FMC3, Cálculo 1 |
Bibliography: |
|
Theoretical course
Topics: | Constructible numbers (straightedge and compass), solutions by radicals, rings, fields, the rational numbers, groups, Galois groups, Galois theory of unsolvability and solvability. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical course
Topics: | Elements of group theory, ring theory, and fields, homomorphism theorems. |
---|---|
Prerequisites: | FMC2 |
Bibliography: |
|
Theoretical course
Topics: | Measurable functions, measures, Lebesgue integration, Decomposition and generation of measures, Product measures, Measurable, nonmeasurable, Borel, non-Borel sets. |
---|---|
Prerequisites: | FMC2, Cálculo 1 (well!) |
Bibliography: |
|
Theoretical course
Topics: | Metric spaces, norms, opened and closed sets, continuity, completeness, compactness, sequences of functions, equicontinuity, topological spaces. |
---|---|
Prerequisites: | FMC2, Cálculo 1 (well!) |
Bibliography: |
|
Theoretical course
Topics: | Topological spaces, continuity, compactness, seperation axioms, Tychonoff theorem. |
---|---|
Prerequisites: | FMC2, Cálculo 1 |
Bibliography: |
|