プログラム言語特論

プログラム言語特論_E
Instructor(s)	Yukiyoshi Kameyama, Hiroshi Unno
E-Mail	{kam, uhiro} [at] cs . tsukuba . ac . jp
URL	http://logic.cs.tsukuba.ac.jp/~kam/acpl/
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.
Goal
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.
TF / TA
Misc.