A Lambda Calculus with Forms

Abstract. The need to use position-dependent parameters often hamdefinition of flexible, extensible, and reusable abstractions for software composition. This observation has led us to explore the concept of forms, which are first-class extensible records and that, in combination with a small set of purely asymmetric operators, provide a core language to address this issue. One interesting application of forms is the definition of contractual specifications to ensure that a component can be safely combined with other components or deployed in a new context. In fact, contractual specifications explicitly and formally state what a component offers without entering into the details of how. In this paper, we develop a formal form-based framework for the definition of contractual specifications. More precisely, we study a substitution-free variant of the lambda-calculus, called λF, where names are replaced with forms and parameter passing is modeled using explicit contexts and show...

• Type: Conference
• Year: 2005
• Where: SOCO
• Authors: Markus Lumpe
• Keywords: Contractual Specifications, Formal Form-based Framework, SOCO 2005, first-class Extensible Records