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!
Minicourses 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. Modeltheoretic, domaintheoretic, 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, finitestate machines, formal languages, grammars, contextfree languages, λcalculus, combinatory logic, primitive recursion, recursive functions, recursive and recursively enumerable sets, smn 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, nonBorel 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: 
