
05173450
j
05173450
Abel, Andreas
Coquand, Thierry
Untyped algorithmic equality for MartinL\"of's logical framework with surjective pairs.
Fundam. Inform. 77, No. 4, 345395 (2007).
2007
IOS Press, Amsterdam; Polish Mathematical Society (Polskie Towarzystwo Matematyczne  PTM), Warsaw
EN
bidirectional type checking algorithm
Summary: MartinL\"of's logical framework is extended by strong $\Sigma$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 $\beta\eta$equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with $\eta$equality on $\beta$normal forms, which is shown equivalent to the algorithmic equality.