Tese de doutoramento Acesso aberto

Type-based termination of recursive definitions and constructor subtyping in typed lambda calculi