§Hi are hypotheses (environments with bindings)
§Ti are terms (pieces of abstract syntax)
§Ri are results (types, run-time values, changed
environments)
§Hj |- Tj : Rj are sequents
§Premises or preconditions are above the
line
§Conclusion is below the line
§Condition on the side if exists must be
satisfied
§