The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi

Simple item page
dc.creatorGacek, Andrew
dc.date2007-02-05
dc.date.accessioned2026-07-07T07:44:40Z
dc.date.available2026-07-07T07:44:40Z
dc.descriptionThe intrinsic treatment of binding in the lambda calculus makes it an ideal data structure for representing syntactic objects with binding such as formulas, proofs, types, and programs. Supporting such a data structure in an implementation is made difficult by the complexity of the substitution operation relative to lambda terms. In this paper we present the suspension calculus, an explicit treatment of meta level binding in the lambda calculus. We prove properties of this calculus which make it a suitable replacement for the lambda calculus in implementation. Finally, we compare the suspension calculus with other explicit treatments of substitution.
dc.description84 pages
dc.identifierhttps://arxiv.org/abs/cs/0702027
dc.identifierhttp://arxiv.org/abs/cs/0702027
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/123282
dc.subjectLogic in Computer Science
dc.subjectProgramming Languages
dc.titleThe Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi
dc.typetext

Files

Collections

arXiv