Name
Abstract | ||
|---|---|---|
We introduce a simply typed λ-calculus λϰƐ" which has both contexts and environments as first-class values. In λϰƐ", holes in contexts are represented by ordinary variables of appropriate types and hole filling is represented by the functional application together with a new abstraction mechanism which takes care of packing and unpacking of the term which is used to fill in the holes of the context. λϰƐ" is a conservative extension of the simply typed λβ-calculus, enjoys subject reduction property, is confluent and strongly normalizing. The traditional method of defining substitution does not work for our calculus. So, we also introduce a new method of defining substitution. Although we introduce the new definition of substitution out of necessity, the new definition turns out to be conceptually simpler than the traditional definition of substitution. |
Year | Venue | Keywords |
|---|---|---|
2001 | FLOPS '01 Proceedings of the 5th International Symposium on Functional and Logic Programming | defining substitution,new definition,new abstraction mechanism,new method,traditional definition,traditional method,appropriate type,conservative extension,first-class value,functional application,Context Calculus,First-Class Environments |
Field | DocType | Volume |
Lambda calculus,Typed lambda calculus,Simply typed lambda calculus,Computer science,Lambda cube,Algorithm,Type inhabitation,Pure type system,Conservative extension,Dependent type,Calculus | Conference | 2002 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-41739-7 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Masahiko Sato | 1 | 0 | 0.34 |
| Takafumi Sakurai | 2 | 46 | 12.45 |
| Yukiyoshi Kameyama | 3 | 171 | 17.29 |