プログラム言語特論

プログラム言語特論_E
Instructor(s)	Yukiyoshi Kameyama, Hiroshi Unno
E-Mail	{kam, uhiro} [at] cs . tsukuba . ac . jp
URL	http://www.cs.tsukuba.ac.jp/~kam/acpl/index.html.en
Office hours	Will be announced in the first lecture.
Cource#	01CH218
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.
relation degree program competence	Knowledge Utilization Skills,Research Skills,Expert Knowledge
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: 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.
TF / TA
Misc.