No Cover Image

Journal article 1200 views

A domain model characterising strong normalisation

Ulrich Berger Orcid Logo

Annals of Pure and Applied Logic, Volume: 156, Issue: 1, Pages: 39 - 50

Swansea University Author: Ulrich Berger Orcid Logo

Full text not available from this repository: check for access using links below.

Abstract

Building on previous work by Coquand and Spiwack we construct a strict domain-theoretic model for the untyped lambda-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not bottom. There are no disjointness or confluence condit...

Full description

Published in: Annals of Pure and Applied Logic
ISSN: 0168-0072
Published: 2008
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa128
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: Building on previous work by Coquand and Spiwack we construct a strict domain-theoretic model for the untyped lambda-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not bottom. There are no disjointness or confluence conditions imposed on the rewrite rules, and under a mild but necessary condition completeness of the method is proven. As an application, we prove strong normalisation for barrecursion in higher types combined with polymorphism and non-deterministic choice.
Keywords: lambda-calculus, term rewriting, normalisation, domain theory
College: Faculty of Science and Engineering
Issue: 1
Start Page: 39
End Page: 50