The surface typechecker is mainly comprised of a constraint generator and a solver. We want to formalise these two components and prove important properties about them. Note that the surface language is not part of the current proof chain (which only starts from the core language) and is not trusted.
Description
The surface typechecker is mainly comprised of a constraint generator and a solver. We want to formalise these two components and prove important properties about them. Note that the surface language is not part of the current proof chain (which only starts from the core language) and is not trusted.