Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs | Zendy

Andreas Abel | Zendy; Thierry Coquand | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs

Author(s) -

Andreas Abel,

Thierry Coquand

Publication year - 2005

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/11417170_4

Subject(s) - surjective function , computer science , equivalence (formal languages) , logical framework , programming language , subroutine , theoretical computer science , algorithm , discrete mathematics , algebra over a field , mathematics , pure mathematics

Martin-Lof's Logical Framework is extended by strong Σ-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped βη-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with η-equality on β-normal forms, which is shown equivalent to the algorithmic equality.

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