Courses and project proposals

Project proposals

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

Develop a web application like SIGAA (but one that works well).
(Could be part/conclusion of an advanced functional programming course.)
Create libraries for proof assistants (Agda, Coq…).
(Could be part/conclusion of a proofs/types/Curry–Howard/verified programming/dependent types course.)
More…

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.

Interactive theorem provers: Agda, Coq
Programming languages:
- Idris
- Racket (LISP)
OpenBSD & firewalling with pf

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