University of Sussex
Browse

File(s) not publicly available

Closed Reduction: explicit substitutions without alpha conversion

journal contribution
posted on 2023-06-08, 08:51 authored by M Fernández, Ian MackieIan Mackie, F-R Sinot
No description supplied

History

Publication status

  • Published

Journal

Mathematical Structures in Computer Science

ISSN

0960-1295

Issue

2

Volume

15

Page range

343-381

Pages

39.0

Department affiliated with

  • Informatics Publications

Notes

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).

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC