On principal types of BCK-lambda-Terms

• Type: Article in International Conference Proceedings Book
• Date: 2007

Authors

Sabine Broda (Author) FCUP; Luis Damas (Author) FCUP

Conference proceedings International

Title: Logic, Language, Information and Computation, Proceedings

Pages: 120-130

14th International Workshop on Logic, Language, Information and Computation

Rio de Janeiro, BRAZIL, JUL 02-05, 2007

Indexing

ISI Web of Knowledge - 0 Citations

Scopus - 0 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

Authenticus ID: P-004-DV9

DOI: 10.1007/978-3-540-73445-1_9

Abstract (EN): Condensed BCK-logic, i.e. the set of BCK-theorems provable by the condensed detachment rule of Carew Meredith, has been shown to be exactly the set of principal types of BCK-lambda-terms. In 1993 Sachio Hirokawa gave a characterization of the set of principal types of BCK-A-terms in beta-normal form based on a relevance relation that he defined between the type variables in a type. We define a symmetric notion of this and call it dependence relation. Then, using the notion of,beta(s)-reduction introduced by de Groote, we obtain a characterization of the complete set of principal types of BCK-lambda-terms.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 11