Closed Reduction: explicit substitutions without alpha conversion

Fernández, M, Mackie, I and Sinot, F-R (2005) Closed Reduction: explicit substitutions without alpha conversion. Mathematical Structures in Computer Science, 15 (2). pp. 343-381. ISSN 0960-1295

Full text not available from this repository.
Item Type: Article
Additional Information: Originality: A novel reduction strategy for computation is defined via a calculus which is free from alpha conversion. The calculus is constrained so that only efficient reductions are allowed. Rigour: All the main properties of the calculus are proved: confluence, preservation of strong normalisation, termination of typed system. Significance: Started a new line of research for programming language implementation, and far reaching applications, for instance in category theory. Impact: This work was an important element to a major result about Godel's System T ("The Power of Linear Functions", CSL 2004; a journal paper is submitted). It was also instrumental to obtain a funded British Council project (UK-Portugal, 2005-2007).
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Ian Mackie
Date Deposited: 06 Feb 2012 21:07
Last Modified: 28 Mar 2012 10:34
📧 Request an update