diff --git a/content/courses/_index.md b/content/courses/_index.md index a4e7e57..a72fd84 100644 --- a/content/courses/_index.md +++ b/content/courses/_index.md @@ -5,6 +5,11 @@ menu = 'main' weight = 60 +++ +## 2023 Fall + +- [COSE 212: Programming Languages]({{< relref "cose212/2023/_index.md" >}}) +- AAA 616: Program Analysis + ## 2023 Spring - [COSE 312: Compilers](https://github.com/kupl-courses/COSE312-2023spring) diff --git a/content/courses/cose212/2023/_index.md b/content/courses/cose212/2023/_index.md new file mode 100644 index 0000000..f3bcc97 --- /dev/null +++ b/content/courses/cose212/2023/_index.md @@ -0,0 +1,44 @@ ++++ +draft = false +title = 'COSE212-23F' ++++ + +# Programming Languages, 2023 Fall + +## Course Information + +- Instructor: [Hakjoo Oh]({{< ref "/members/hakjoo-oh" >}}) +- TAs: [Minsu Kim]({{< "/members/minsu-kim" >}}), Doyeon Hwang +- Lecture: 09:00-11:45 on Mondays and Wednesday (8 weeks) +- [Syllabus](./syllabus.pdf) + +## References + +- [프로그래밍 언어의 원리](./pl-book.pdf) +- [Essentials of Programming Languages](https://www.amazon.com/gp/product/0262062798?ie=UTF8&tag=ucmbread-20&linkCode=as2&camp=1789&creative=9325&creativeASIN=0262062798) +- [Notes on Programming Languages (in Korean)](./pl-book-draft.pdf) + +## Slides + +- Course Overview: [lec0.pdf](./slides/lec0.pdf) +- (Part 1) Preliminaries + - Inductive Definitions: [lec1.pdf](./slides/lec1.pdf), [lec2.pdf](./slides/lec2.pdf) + - Functional Programming: [lec3.pdf](./slides/lec3.pdf), [lec4.pdf](./slides/lec4.pdf) +- (Part 2) Basic Concepts + - Expressions: [lec5.pdf](./slides/lec5.pdf), [code](./slides/let.ml) + - Procedures: [lec6.pdf](./slides/lec6.pdf) + - Lexical scoping: [lec7.pdf](./slides/lec7.pdf) + - States: [lec8.pdf](./slides/lec8.pdf) + - Records, Pointers, and garbage collection: [lec9.pdf](./slides/lec9.pdf) +- (Part 3) Advanced Concepts + - Static Type System: [lec10.pdf](./slides/lec10.pdf), [lec11.pdf](./slides/lec11.pdf), [lec12.pdf](./slides/lec12.pdf) + - Automatic Type Inference: [lec13.pdf](./slides/lec13.pdf), [lec14.pdf](./slides/lec14.pdf), [lec15.pdf](./slides/lec15.pdf) + - Polymorphic Type System: [lec16.pdf](./slides/lec16.pdf) + - Lambda Calculus: [lec17.pdf](./slides/lec17.pdf) + - Operational and denotational semantics: [lec18.pdf](./slides/lec18.pdf) +- Course Review: [lec19.pdf](./slides/lec19.pdf) + +## Programming Assignment + +- Programming exercises: [ocaml-exercises.pdf](./hw/ocaml-exercises.pdf) +- Final Project (interpreter and type checker): [project.pdf](./hw/project.pdf) [template](./hw/ml_minus.ml) diff --git a/content/courses/cose212/2023/hw/ml_minus.ml b/content/courses/cose212/2023/hw/ml_minus.ml new file mode 100644 index 0000000..d756b67 --- /dev/null +++ b/content/courses/cose212/2023/hw/ml_minus.ml @@ -0,0 +1,255 @@ +(* Do not open any module *) + +(***********************) +(* Library functions *) +(***********************) + +let rec fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a += fun f accu lst -> + match lst with + | [] -> accu + | hd::tl -> fold_left f (f accu hd) tl + +let rec map : ('a -> 'b) -> 'a list -> 'b list += fun f lst -> + match lst with + | [] -> [] + | hd::tl -> (f hd)::(map f tl) + +(***********************) +(****** Syntax *******) +(***********************) + +type program = exp +and exp = + | UNIT + | TRUE + | FALSE + | CONST of int + | VAR of var + | ADD of exp * exp + | SUB of exp * exp + | MUL of exp * exp + | DIV of exp * exp + | EQUAL of exp * exp + | LESS of exp * exp + | NOT of exp + | NIL + | CONS of exp * exp + | APPEND of exp * exp + | HEAD of exp + | TAIL of exp + | ISNIL of exp + | IF of exp * exp * exp + | LET of var * exp * exp + | LETREC of var * var * exp * exp + | LETMREC of (var * var * exp) * (var * var * exp) * exp + | PROC of var * exp + | CALL of exp * exp + | PRINT of exp + | SEQ of exp * exp +and var = string + +(***********************) +(** Example programs **) +(***********************) + +(* + let f = proc (x) (x - 11) + in (f (f 77)) +*) +let proc1 = + LET ("f", PROC ("x", SUB (VAR "x", CONST 11)), + CALL (VAR "f", CALL (VAR "f", CONST 77))) + +(* + ((proc (f) (f (f 77))) (proc (x) (x-11))) +*) +let proc2 = + CALL (PROC ("f", CALL (VAR "f", CALL (VAR "f", CONST 77))), + PROC ("x", SUB (VAR "x", CONST 11))) + +(* + let x = 1 + in let f = proc (y) (x + y) + in let x = 2 + in let g = proc (y) (x + y) + in (f 1) + (g 1) +*) +let let1 = + LET ("x", CONST 1, + LET ("f", PROC ("y", ADD (VAR "x", VAR "y")), + LET ("x", CONST 2, + LET ("g", PROC ("y", ADD (VAR "x", VAR "y")), + (ADD (CALL (VAR "f", CONST 1), + CALL (VAR "g", CONST 1))))))) + +(* + letrec even(x) = if (x = 0) then true else odd(x-1) + odd(x) = if (x = 0) then false else even(x-1) + in (even 13) +*) +let evenodd = + LETMREC (("even", "x", IF (EQUAL (VAR "x", CONST 0), TRUE, CALL (VAR "odd", SUB (VAR "x", CONST 1)))), + ("odd" , "x", IF (EQUAL (VAR "x", CONST 0), FALSE, CALL (VAR "even", SUB (VAR "x", CONST 1)))), + CALL (VAR "odd", CONST 13)) + + +(* + letrec double(x) = if (x = 0) then 0 else (double (x-1) + 2 + in (double 6) +*) +let double = + LETREC ("double", "x", IF (EQUAL (VAR "x", CONST 0), + CONST 0, + ADD (CALL (VAR "double", SUB (VAR "x", CONST 1)) , + CONST 2)), + CALL (VAR "double", CONST 6)) + +(* +letrec factorial(x) = + if (x = 0) then 1 + else factorial(x-1) * x +in letrec loop n = + if (n = 0) then () + else (print (factorial n); loop (n-1)) + in (loop 10) +*) +let fact = +LETREC ("factorial", "x", + IF (EQUAL (VAR "x", CONST 0), CONST 1, + MUL (CALL (VAR "factorial", SUB (VAR "x", CONST 1)), VAR "x")), + LETREC ("loop", "n", + IF (EQUAL (VAR "n", CONST 0), UNIT, + SEQ (PRINT (CALL (VAR "factorial", VAR "n")), + CALL (VAR "loop", SUB(VAR "n", CONST 1)))), + CALL (VAR "loop", CONST 10))) + +(* +in letrec range(n) = + if (n = 1) then (cons 1 nil) + else n::(range (n-1)) +in (range 10) +*) +let range = +LETREC ("range", "n", + IF (EQUAL (VAR "n", CONST 1), CONS (CONST 1, NIL), + CONS (VAR "n", CALL (VAR "range", SUB (VAR "n", CONST 1)))), + CALL (VAR "range", CONST 10)) + +(* +letrec reverse(l) = + if (isnil l) then [] + else (reverse (tl l)) @ (cons hd l) +in (reverse (cons (1, cons (2, cons (3, nil))))) +*) +let reverse = +LETREC ("reverse", "l", + IF (ISNIL (VAR "l"), NIL, + APPEND (CALL (VAR "reverse", TAIL (VAR "l")), + CONS (HEAD (VAR "l"), NIL))), + CALL (VAR "reverse", + CONS (CONST 1, CONS (CONST 2, CONS (CONST 3, NIL))))) + +let reverse2 = +LETREC ("reverse", "l", + IF (ISNIL (VAR "l"), NIL, + APPEND (CALL (VAR "reverse", TAIL (VAR "l")), + CONS (HEAD (VAR "l"), NIL))), + CALL (VAR "reverse", + CONS (CONS (CONST 1, NIL), CONS (CONS (CONST 2, NIL), CONS (CONS (CONST 3, NIL), NIL))))) + + +let zfact = + LET ("fix", + PROC ("f", + CALL (PROC ("x", CALL (VAR "f", PROC ("y", CALL (CALL (VAR "x", VAR "x"), VAR "y")))), + PROC ("x", CALL (VAR "f", PROC ("y", CALL (CALL (VAR "x", VAR "x"), VAR "y")))))), + LET ("f", CALL (VAR "fix", + PROC ("f", PROC ("x", + IF (EQUAL (VAR "x", CONST 0), CONST 1, + MUL (CALL (VAR "f", SUB (VAR "x", CONST 1)), VAR "x"))))), + CALL (VAR "f", CONST 10))) + +let zrange = + LET ("fix", + PROC ("f", + CALL (PROC ("x", CALL (VAR "f", PROC ("y", CALL (CALL (VAR "x", VAR "x"), VAR "y")))), + PROC ("x", CALL (VAR "f", PROC ("y", CALL (CALL (VAR "x", VAR "x"), VAR "y")))))), + + + LET ("f", CALL (VAR "fix", + PROC ("range", PROC ("n", + IF (EQUAL (VAR "n", CONST 1), CONS (CONST 1, NIL), + CONS (VAR "n", CALL (VAR "range", SUB (VAR "n", CONST 1))))))), + CALL (VAR "f", CONST 10))) + +let poly = + LET ("f", PROC("x", VAR "x"), + IF(CALL (VAR "f", TRUE), CALL (VAR "f", CONST 1), CALL (VAR "f", CONST 2))) + +let lst = + CONS (CONST 1, CONS (CONST 2, CONS (TRUE, NIL))) + +(***********************) +(***** Problem 1 *****) +(***********************) + +type value = + | Unit + | Int of int + | Bool of bool + | List of value list + | Procedure of var * exp * env + | RecProcedure of var * var * exp * env + | MRecProcedure of var * var * exp * + var * var * exp * env +and env = (var * value) list + +exception UndefinedSemantics + +let rec string_of_value v = + match v with + | Int n -> string_of_int n + | Bool b -> string_of_bool b + | List lst -> "[" ^ fold_left (fun s x -> s ^ ", " ^ x) "" (map string_of_value lst) ^ "]" + | _ -> "(functional value)" + +let empty_env = [] +let extend_env (x,v) e = (x,v)::e +let rec lookup_env x e = + match e with + | [] -> raise (Failure ("variable " ^ x ^ " is not bound in env")) + | (y,v)::tl -> if x = y then v else lookup_env x tl + +let rec eval : exp -> env -> value +=fun exp env -> + match exp with + | PRINT e -> (print_endline (string_of_value (eval e env)); Unit) + | _ -> raise (Failure "Not implemented") (* TODO *) + +let runml : program -> value +=fun pgm -> eval pgm empty_env + + +(***********************) +(***** Problem 2 *****) +(***********************) + +type typ = + TyUnit + | TyInt + | TyBool + | TyFun of typ * typ + | TyList of typ + | TyVar of tyvar +and tyvar = string + +exception TypeError + +(* You can invoke "fresh_tyvar()" to generate a fresh type variable *) +let tyvar_num = ref 0 +let fresh_tyvar () = (tyvar_num := !tyvar_num + 1; (TyVar ("t" ^ string_of_int !tyvar_num))) + +let typecheck : program -> typ +=fun exp -> raise TypeError (* TODO *) \ No newline at end of file diff --git a/content/courses/cose212/2023/hw/ocaml-exercises.pdf b/content/courses/cose212/2023/hw/ocaml-exercises.pdf new file mode 100644 index 0000000..892ed3f Binary files /dev/null and b/content/courses/cose212/2023/hw/ocaml-exercises.pdf differ diff --git a/content/courses/cose212/2023/hw/project.pdf b/content/courses/cose212/2023/hw/project.pdf new file mode 100644 index 0000000..f11edeb Binary files /dev/null and b/content/courses/cose212/2023/hw/project.pdf differ diff --git a/content/courses/cose212/2023/pl-book-draft.pdf b/content/courses/cose212/2023/pl-book-draft.pdf new file mode 100644 index 0000000..78ee532 Binary files /dev/null and b/content/courses/cose212/2023/pl-book-draft.pdf differ diff --git a/content/courses/cose212/2023/pl-book.pdf b/content/courses/cose212/2023/pl-book.pdf new file mode 100644 index 0000000..9114fc7 Binary files /dev/null and b/content/courses/cose212/2023/pl-book.pdf differ diff --git a/content/courses/cose212/2023/slides/lec0.pdf b/content/courses/cose212/2023/slides/lec0.pdf new file mode 100644 index 0000000..bc3895b Binary files /dev/null and b/content/courses/cose212/2023/slides/lec0.pdf differ diff --git a/content/courses/cose212/2023/slides/lec1.pdf b/content/courses/cose212/2023/slides/lec1.pdf new file mode 100644 index 0000000..248b2f9 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec1.pdf differ diff --git a/content/courses/cose212/2023/slides/lec10.pdf b/content/courses/cose212/2023/slides/lec10.pdf new file mode 100644 index 0000000..7f85aa2 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec10.pdf differ diff --git a/content/courses/cose212/2023/slides/lec11.pdf b/content/courses/cose212/2023/slides/lec11.pdf new file mode 100644 index 0000000..bbb1e84 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec11.pdf differ diff --git a/content/courses/cose212/2023/slides/lec12.pdf b/content/courses/cose212/2023/slides/lec12.pdf new file mode 100644 index 0000000..3fb87bc Binary files /dev/null and b/content/courses/cose212/2023/slides/lec12.pdf differ diff --git a/content/courses/cose212/2023/slides/lec13.pdf b/content/courses/cose212/2023/slides/lec13.pdf new file mode 100644 index 0000000..c138ff8 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec13.pdf differ diff --git a/content/courses/cose212/2023/slides/lec14.pdf b/content/courses/cose212/2023/slides/lec14.pdf new file mode 100644 index 0000000..c4b1a30 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec14.pdf differ diff --git a/content/courses/cose212/2023/slides/lec15.pdf b/content/courses/cose212/2023/slides/lec15.pdf new file mode 100644 index 0000000..09b65e6 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec15.pdf differ diff --git a/content/courses/cose212/2023/slides/lec16.pdf b/content/courses/cose212/2023/slides/lec16.pdf new file mode 100644 index 0000000..9d3e7b0 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec16.pdf differ diff --git a/content/courses/cose212/2023/slides/lec17.pdf b/content/courses/cose212/2023/slides/lec17.pdf new file mode 100644 index 0000000..2cee08f Binary files /dev/null and b/content/courses/cose212/2023/slides/lec17.pdf differ diff --git a/content/courses/cose212/2023/slides/lec18.pdf b/content/courses/cose212/2023/slides/lec18.pdf new file mode 100644 index 0000000..443b07e Binary files /dev/null and b/content/courses/cose212/2023/slides/lec18.pdf differ diff --git a/content/courses/cose212/2023/slides/lec19.pdf b/content/courses/cose212/2023/slides/lec19.pdf new file mode 100644 index 0000000..127dc03 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec19.pdf differ diff --git a/content/courses/cose212/2023/slides/lec2.pdf b/content/courses/cose212/2023/slides/lec2.pdf new file mode 100644 index 0000000..eb79f39 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec2.pdf differ diff --git a/content/courses/cose212/2023/slides/lec3.pdf b/content/courses/cose212/2023/slides/lec3.pdf new file mode 100644 index 0000000..5968595 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec3.pdf differ diff --git a/content/courses/cose212/2023/slides/lec4.pdf b/content/courses/cose212/2023/slides/lec4.pdf new file mode 100644 index 0000000..bcaa6a2 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec4.pdf differ diff --git a/content/courses/cose212/2023/slides/lec5.pdf b/content/courses/cose212/2023/slides/lec5.pdf new file mode 100644 index 0000000..12c20ab Binary files /dev/null and b/content/courses/cose212/2023/slides/lec5.pdf differ diff --git a/content/courses/cose212/2023/slides/lec6.pdf b/content/courses/cose212/2023/slides/lec6.pdf new file mode 100644 index 0000000..d57f479 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec6.pdf differ diff --git a/content/courses/cose212/2023/slides/lec7.pdf b/content/courses/cose212/2023/slides/lec7.pdf new file mode 100644 index 0000000..2971487 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec7.pdf differ diff --git a/content/courses/cose212/2023/slides/lec8.pdf b/content/courses/cose212/2023/slides/lec8.pdf new file mode 100644 index 0000000..18536bc Binary files /dev/null and b/content/courses/cose212/2023/slides/lec8.pdf differ diff --git a/content/courses/cose212/2023/slides/lec9.pdf b/content/courses/cose212/2023/slides/lec9.pdf new file mode 100644 index 0000000..589e3b4 Binary files /dev/null and b/content/courses/cose212/2023/slides/lec9.pdf differ diff --git a/content/courses/cose212/2023/slides/let.ml b/content/courses/cose212/2023/slides/let.ml new file mode 100644 index 0000000..c9bcd10 --- /dev/null +++ b/content/courses/cose212/2023/slides/let.ml @@ -0,0 +1,77 @@ +(* +1. store this file as a file (e.g. "let.ml") +2. type "ocaml let.ml" in the shell command line +*) + +type pgm = exp +and exp = + | CONST of int + | VAR of string + | ADD of exp * exp + | SUB of exp * exp + | ISZERO of exp + | IF of exp * exp * exp + | LET of string * exp * exp + | READ + +(* +let x = 1 in + let y = let x = 2 + in x + x + in x + y +*) +let pgm1 = + LET ("x", CONST 1, + LET ("y", LET ("x", CONST 2, + ADD (VAR "x", VAR "x")), + (ADD (VAR "x", VAR "y")))) + +type value = Int of int | Bool of bool + +module Env = struct + type t = (string * value) list + let empty = [] + let rec lookup x e = + match e with + | [] -> raise (Failure ("Env: Not found: " ^ x)) + | (y,v)::tl -> + if y = x then v else lookup x tl + let update x v e = (x,v)::e +end + +let rec eval : Env.t -> exp -> value +=fun env exp -> + match exp with + | CONST n -> Int n + | VAR x -> Env.lookup x env + | ADD (e1, e2) -> binop env e1 e2 (+) + | SUB (e1, e2) -> binop env e1 e2 (-) + | READ -> Int (read_int ()) + | ISZERO e -> + (match eval env e with + | Int 0 -> Bool true + | Int _ -> Bool false + | _ -> raise (Failure "type error")) + | IF (e1,e2,e3) -> + (match eval env e1 with + | Bool true -> eval env e2 + | Bool false -> eval env e3 + | _ -> raise (Failure "type error")) + | LET (x,e1,e2) -> + let v1 = eval env e1 in + let v = eval (Env.update x v1 env) e2 in + v + +and binop env e1 e2 op = + let v1 = eval env e1 in + let v2 = eval env e2 in + match v1, v2 with + | Int n1, Int n2 -> Int (op n1 n2) + | _ -> raise (Failure ("type error")) + +let print_value v = + print_endline (match v with + | Int n -> string_of_int n + | Bool b -> string_of_bool b) + +let _ = print_value (eval Env.empty pgm1) diff --git a/content/courses/cose212/2023/syllabus.pdf b/content/courses/cose212/2023/syllabus.pdf new file mode 100644 index 0000000..168a661 Binary files /dev/null and b/content/courses/cose212/2023/syllabus.pdf differ