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 at the first lecture.
Cource# 01CH212
Area Intelligent Software
Basic/Advanced 専門科目
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.
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: Unno)
  • Lambda calculus and type system
  • Program Verification using Refinement Types
  • Program Verification: Tools and Examples
Second half (Instructor: Kameyama)
  • Metaprogramming, program generation
  • Program Generation: language, type system and safety
  • Program Generation: examples and applications
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 exercises (30%) and final examination (70%) assuming that students attend all lectures.