A proof of strong normalisation using domain theory

Details A proof of strong normalisation using domain theory A proof of strong normalisation using domain theory

2007-09-10

arxiv.org/abs/0709.1401v2

LMCS 3 (4:12) 2007

Computer Science

Logic in Computer Science

16 pages

Scientific paper

10.2168/LMCS-3(4:12)2007

Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recursion. The main contribution of this paper is to show that, using ideas from intersection types and Martin-Lof's domain interpretation of type theory one can in turn simplify further U. Berger's argument. We build a domain model for an untyped programming language where U. Berger has an interpretation only for typed terms or alternatively has an interpretation for untyped terms but need an extra condition to deduce strong normalisation. As a main application, we show that Martin-L\"{o}f dependent type theory extended with a program for Spector double negation shift.

Affiliated with

Also associated with

No associations

Rating

A proof of strong normalisation using domain theory does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A proof of strong normalisation using domain theory, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A proof of strong normalisation using domain theory will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-656302