Haskell CS 421 LogoCS 421 — Programming Languages

Monotype Proof Tree Editor

Monotype Derivation

Write a proof tree for the following judgement:

Γif f 00 then f else (λx. x):IntInt\Gamma \vdash \mathtt{if}\ f\ 0 \ge 0 \ \mathtt{then}\ f\ \mathtt{else}\ (\lambda x.\ x) : Int \to Int

Let f:IntIntf : Int \rightarrow Int in Γ\Gamma.

Each line of your tree should have the following components:

  1. a number followed by a period to indicate its depth in the tree. 0 is the root.
  2. a Gamma, in the form G, Gnn (where nn is an integer) or as a set of variable type assignments.
  3. The |- operator.
  4. An expression.
  5. The : operator.
  6. A type name. Type names are capitalized.
  7. A rule name in parenthesis.

If you use G or G1, etc. in your proof tree, you must follow the tree with their expanded out definitions.

The starter code shows a valid tree for a proof of Γx+y:Int\Gamma \vdash x + y : Int.

Here are the monotype rules.

Proof Tree Editor

Score: 17.61%
Γx:IntVARΓy:IntVARΓx+y:IntBINOP\frac{\frac{}{\displaystyle \Gamma\vdash x : Int} \textstyle \mathrm{V\small{AR}} \quad \frac{}{\displaystyle \Gamma\vdash y : Int} \textstyle \mathrm{V\small{AR}}}{\displaystyle \Gamma\vdash x + y : Int}\textstyle \mathrm{B\small{INOP}}