Lg

• The universe of Lg are consistent global typing contexts together with ?,

• (?1, A1) ? (?2, A2) to be (?1 ? ?2, A1 ? A2) if (?1 ? ?2, A1 ? A2) is consistent and ? otherwise.

• (?1, A1) ? (?2, A2) if ?2 ? ?1 and A2 ? A1.

Previous slide

Next slide

Back to first slide

View graphic version