Computer Science – Logic in Computer Science
Scientific paper
2006-11-09
Computer Science
Logic in Computer Science
44 pages, final version for ToCL (with minor changes wrt previous)
Scientific paper
The formal system lambda-delta is a typed lambda calculus that pursues the unification of terms, types, environments and contexts as the main goal. lambda-delta takes some features from the Automath-related lambda calculi and some from the pure type systems, but differs from both in that it does not include the Pi construction while it provides for an abbreviation mechanism at the level of terms. lambda-delta enjoys some important desirable properties such as the confluence of reduction, the correctness of types, the uniqueness of types up to conversion, the subject reduction of the type assignment, the strong normalization of the typed terms and, as a corollary, the decidability of type inference problem.
No associations
LandOfFree
The Formal System lambda-delta does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with The Formal System lambda-delta, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The Formal System lambda-delta will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-407700