University of Tsukuba | Grad. Scho. Syst. and Info. Eng. | Dept. Comp. Sci. | List of Courses
Yukiyoshi Kameyama, Hiroshi Unno
E-Mail {kam, uhiro} [at] cs . tsukuba . ac . jp
Office hours Will be announced in the first lecture.
Cource# 01CH218
Area Intelligent Software
Course style Lectures
Term SprAB
Period Tue2
Room# 3B302
Keywords Functional Programming, Type System, Lambda Calculus, Program Generation, Program Verification.
Prerequisites Basic knowledge about at least one functional programming languages such as Lisp, Scheme, ML (SML, OCaml, F#), and Haskell.
relation degree program competence Knowledge Utilization Skills,Research Skills,Expert Knowledge
Outline Students learn a few topics of latest research in functional programming and type theories, in particular, their applications and technical background. Students also do exercises and write reports using a functional programming language.
Course plan First half (Instructor: Kameyama)
  • Lambda calculus and type system
  • Metaprogramming, program generation
  • Program Generation: language, type system and safety
  • Program Generation: examples and applications
Second half (Instructor: Unno)
  • Program Verification based on Refinement Types
  • Program Verification based on Automated Theorem Proving and Constraint Solving
Textbook Course handouts will be put on the course home page.
References B. C. Pierce, "Types and Programming Languages", MIT Press, 2022.
Evaluation Based on reports, assuming that students attend all lectures.