Course, mini-course, and project proposals

(In reverse order, because why not…)

Project proposals

Some ideas for projects with students of IMD. Interested students, should contact me ASAP!

Mini-course proposals

Mini-courses I have already offered are available on my teaching website. The following are proposals to consider, in case there is interest.

Course proposals

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.

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:
  • Nederpelt & Geuvers: Type Theory and Formal proof
  • Thompson: Type Theory & Functional Programming
  • Girard: Proofs and Types
  • Sørensen & Urzyczyn: Lectures on the Curry–Howard isomorphism

Denotational semantics of programming languages

Theoretical course

Topics: Denotational semantics of imperative, functional, and logic programming languages. Model-theoretic, domain-theoretic, and game semantics.
Prerequisites:FMC2
Bibliography:
  • Stoy: Denotational Semantics
  • Lloyd: Foundations of Logic Programming
  • Tennent: Semantics of Programming Languages
  • Laurent: notes on game semantics

Functional programming

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:
  • Hutton: Programming in Haskell
  • Bird: Introduction to Functional Programming
  • Bird: Thinking Functionally with Haskell
  • Lipovača: LYAH
Possible projects: Develop a web application like SIGAA; extend xmonad; clone xmonad; implement a simple programming language.

Programming with Higher-Order Logic

Theoretical and practical course

Topics: Introduction to λProlog and proof search.
Prerequisites:FMC3, some experience (theoretical or practical) with logic programming
Bibliography:
  • Miller & Nadathur: Programming with Higher-Order Logic

Types and programming languages

Theoretical and practical course

Topics: Untyped systems, Simple types, Subtyping, Recursive Types, Polymorphism.
Prerequisites:FMC2
Bibliography:
  • Pierce: Types and Programming Languages
  • Harper: Practical Foundations for Programming Languages
Possible projects: Implement and extend some of Pierce's systems in Haskell, Agda, or Idris.

Lambda calculus and combinatory logic

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:
  • Krivine: Lambda calculus
  • Hindley & Seldin: λ-calculus and Combinators
  • Girard: Proofs and types

Set theory

Theoretical course

Topics: Axiomatic set theory, ZFC, Choice, Ordinals, Cardinals, Independence proofs.
Prerequisites:FMC2
Bibliography:
  • Moschovakis: Notes on Set theory
  • Kunen: Set theory
  • Jech: Set theory

Category theory

Theoretical course

Topics: Categories, Diagrams, Functors, Natural transformations, Cartesian closed categories, Limits/Colimits.
Prerequisites:FMC2
Bibliography:
  • Lawvere & Schanuel: Conceptual Mathematics: A first introduction to categories
  • Lawvere & Rosebrugh: Sets for Mathematics
  • Awodey: Category theory
  • Barr & Wells: Category Theory for Computing Science

Lattice, order, and domain theory

Theoretical course

Topics: Posets, Lattices, Distributive lattices, Complete lattices, CPOs, Domains, fixpoint theorems.
Prerequisites:FMC2
Bibliography:
  • Davey & Priestley: Lattices and Order
  • Grätzer: Lattice theory: foundation

Recursion theory and computability

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:
  • Cutland: Computability
  • Rogers: Theory of recursive functions
  • Moschovakis: notes on recursion and computation
  • Kleene: Introduction to Metamathematics
  • Hopcroft & Ullman: Introduction to Automata theory, Languages, and Computation

Mathematical logic

Theoretical course

Topics: Propositional and Predicate calculus, Completeness, Incompleteness.
Prerequisites:FMC2
Bibliography:
  • Cori & Lascar: Mathematical Logic
  • Shoenfield: Mathematical Logic
  • Kunen: Foundations of Mathematics
  • Smullyan: First-order logic

Topology via logic

Theoretical course

Topics: Posets, lattices, frames, Heyting algebras, topology, continuity, Scott topology, compactness, locales, Domain theory.
Prerequisites:FMC3, Cálculo 1
Bibliography:
  • Vickers: Topology via Logic

Algebra (Galois theory)

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:
  • Stillwell: Elements of Algebra
  • Birkhoff & Mac Lane: A survey of modern algebra
  • Mac Lane & Birkhoff: Algebra

Algebra (Groups, rings, fields)

Theoretical course

Topics: Elements of group theory, ring theory, and fields, homomorphism theorems.
Prerequisites:FMC2
Bibliography:
  • Herstein: Topics in Algebra
  • Birkhoff & Mac Lane: A survey of modern algebra
  • Mac Lane & Birkhoff: Algebra

Measure theory

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:
  • Bartle: The Elements of Integration and Lebesgue Measure
  • Halmos: Measure theory

Real analysis

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:
  • Carothers: Real Analysis
  • Simmons: Topology and modern analysis
  • Kolmogorov & Fomin: Elements of the Theory of Functions and Functional Analysis
  • Tao: Analysis I

General topology

Theoretical course

Topics: Topological spaces, continuity, compactness, seperation axioms, Tychonoff theorem.
Prerequisites:FMC2, Cálculo 1
Bibliography:
  • Willard: General topology
  • Munkres: Topology
  • Simmons: Topology and modern analysis
  • Rundle: A taste of topology