Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-73445-1_9 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
typed lambda-calculus,principal types,condensed BCK-logic | Discrete mathematics,Computer science,Lambda | Conference |
Volume | ISSN | Citations |
4576 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 1 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sabine Broda | 1 | 64 | 13.83 |
| Luís Damas | 2 | 128 | 22.34 |