A Partial Type Checking Algorithm for Type:Type | Zendy

Andreas Abel | Zendy; Thorsten Altenkirch | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Partial Type Checking Algorithm for Type:Type

Author(s) -

Andreas Abel,

Thorsten Altenkirch

Publication year - 2011

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2011.02.013

Subject(s) - coinduction , type (biology) , dependent type , algorithm , mathematics , computation , type theory , domain (mathematical analysis) , type inference , computer science , programming language , discrete mathematics , lambda calculus , mathematical proof , artificial intelligence , ecology , mathematical analysis , geometry , biology , inference

We analyze a partial type checking algorithm for the inconsistent domain-free pure type system Type:Type (λ⁎). We show that the algorithm is sound and partially complete using a coinductive specification of algorithmic equality. This entails that the algorithm will only diverge due to the presence of diverging computations, in particular it will terminate for all typeable terms

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research