Problem 1
a) -1pt if you specified return type, but no argument types
b) -1pt if you did not specify that the resulting function has one integer argument
   -2pt if it is not clear from your answer that a function after partial function application is returned
c) -2pt for claiming no value is returned, but no explanation
   -1pt for not explaining the type error


Problem 2
-1pt for using let instead of let rec
-1pt for wrong matching case (for example, trying to match list with a single integer)
-2pt for not maintaining the prefix of the returned list (in the tail recursive implementation)
-1pt for returning the wrong value in the base case (e.g., n instead of [n] or n :: [])
-1pt for inserting at the wrong position in the list (i.e., if the element would not be
     inserted immediately before the first element that is greater than n)
-1pt for skipping head of the list in the result (e.g., by concatenating the element n to the tail of 
     the list, or by not concatenating the head of the list in the recursive call with only the element
	 n and the tail)


Problem 3 (13pt)
-2pt for each update operator
-1pt if final environment does not have m->1 and n->2
-6pt if f is substantially different from f -> <x -> y -> (m*x)+(n*y),env>
-1pt if f does not use the same notation as in the HW
-2pt if m,n is applied directly in the function body, e.g. "f -> < x -> y -> x + 2y, env>"
-3pt if the environment of f is missing some bindings
-3pt for using tuples for f, i.e. f -> < (x,y) -> ... >
-6pt if y is substantially different from y -> < y -> (m*x)+(n*y), env> 
-1pt if y does not use the same notation as in the HW
-2pt if m,n,x is applied directly in the function body, e.g. "y -> < y -> 3 + 2y, env>"
-3pt if the environment of y is missing some bindings
-3pt if y accepts 2 parameters
-1pt for minor errors, such as mismatching brackets that may lead to misinterpretation of the answer


Problem 4 (16pt).
* part 1 (7pt)
-2pt if the function is not forward recursive
-1pt for counting instead of computing the sum
-1pt for using library functions
-2pt for adding pairs
* part 2 (9pt)
-1pt for counting instead of computing the sum
-1pt for using library functions
-2pt for adding pairs


Problem 5 (10pt).
(a) -4pt for k (g 2)
(b) -6pt for k g 2
(c) -4pt for k (g 2 (f x -> x))
(d) -6pt for g k 2
(e) -6pt for g 2 (fun x -> x)


Problem 6 (17pt).
* 7pt for correctly matching on AppExp and choosing free variables v1 and v2
* 10pt for correctly using constructors ContCPS and AppCps and making the recursive calls to cps_exp
-2pt for using kx for fresh variables in constructor ContCPS
-1pt for each wrong argument order in constructors ContCPS and AppCps
-1pt for using cps_exp as if it returns exp_cps instead of exp_cps * int 
-1pt for using kx (or kx + 1, kx + 2, etc) for the second recursive call to cps_exp instead of using the
     second element of the pair returned by the first call to cps_exp


Problem 7
a) -4pt for not specifying appropriate recursive type in the variant definition
   -3pt for not specifying a polymorphic variant, but need to have both correct base type and recursive  type
   -1pt for missing polymorphic specification in the type name (e.g., no 'a in type nonemptylist), but 
        using polymorphism correctly in the base and recursive type definitions
   -1pt for omitting polymorphic type in the recursive type while using polymorphism in the type name
b) -4pt for correct logic, but using Ocaml lists or a type that allows empty lists 
   -3pt for handling recursive case incorrectly by not multiplying head with recursive call to the tail
   -2pt for handling base case incorrectly by not returning the single (only) element of the current list


Problem 8
a) -1pt if you did not label each rule you applied
b) -1pt if you did not give names to pieces of proof tree that you used somewhere else
c) -1pt if you did not write the type environments consistently as maps from variables to their types;
        no + or other operations on environments are needed in concrete type derivations.
d) -2pt if you did not apply the instance of the LET rule correctly (empty environment, mentioning the expected type
e) -1pt if you did not write the correct type judgement for true: {} |- true : bool
f) -1pt if you did not write the correct type judgement for fun f -> ... : {x:bool} |- fun f -> (f x) * 7 : (bool -> int) -> int
g) -1pt if you did not say it that the type judgement at e) follows by the CONST rule
h) -2pt if you did not apply the FUN rule correctly on the type judgement at f)  (similarly for the ARITH rule)
i) -1pt if you did not write the correct type judgement for body of the function: {x:bool, f:bool->int} |- (f x) * 7 : int
j) -1pt if you did not write the correct type judgement for f x
k) -1pt if you did not apply the CONST rule for 7
l) -2pt if you did not apply the APP rule in order to type f x
m) -1pt if you did not use VAR to derive the type of x to be bool
n) -1pt if you did not write the correct type judgement for f
o) -1pt if you did not use VAR to derive the type of f to be bool -> int


Problem 9 (10pt)
Since this is a bonus problem, it was graded more harsh than the normal problems.
-5pt if the beginning environment from problem 3 is incorrect
-10pt if no function application was shown
-5pt if App was not used correctly, e.g. the parameter was not evaluated first, the environment was not swapped + updated after the application
-5pt if for more than 2 occurrences, Eval does not include the environment
-5pt for not using Eval and explaining in plain words