مرکز منطقه ای اطلاع رساني علوم و فناوري - A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

Title of article :

A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

Author/Authors :

René Vestergaard، نويسنده , , James Brotherston، نويسنده ,

Issue Information :

روزنامه با شماره پیاپی سال 2003

Pages :

From page :

212

To page :

244

Keywords :

k-Calculus , confluence , Theorem proving , Barendregt s VariableConvention , Structural induction and recursion

Journal title :

Information and Computation

Serial Year :

2003

Journal title :

Information and Computation

Record number :

333736

Link To Document :