Erik Poll

• A programming logic based on type theory