layout: strict-home-rr title: “JFLP: Volume 2000, Article 1”

The Journal of Functional and Logic Programming

Volume 2000

Article 1

Published by The MIT Press . Copyright 2000 Massachusetts Institute of Technology.

----------------------------------------------------------------

Metatheoretic Results for a Modal lambda-Calculus

Joelle Despeyroux and Pierre Leleu

31 January 2000

Abstract

This paper presents the proofs of the strong normalization, subject reduction, and Church-Rosser theorems for a presentation of the intuitionistic modal lambda-calculus S4. It is adapted from Healfdene Goguen's thesis, where these properties are shown for the simply typed lambda-calculus and for Luo's type theory UTT. Following this method, we introduce the notion of typed operational semantics for our system. We define a notion of typed substitution for our system, which has context stacks instead of the usual contexts. This latter peculiarity leads to the main difficulties and consequently to the main original features in our proofs. The techniques elaborated in this work have already been found useful in recent works [DesLel98,DesLel99] and should be further exploited to prove the properties of other systems based on modality.
The following versions of the article are available: You can find this article also on the ftp-server of The MIT Press (access may be faster from some sites).

----------------------------------------------------------------

Self citation 

    @article{jflp2000-01,
      author={Joelle Despeyroux and Pierre Leleu},
      title={Metatheoretic Results for a Modal lambda-Calculus},
      journal={Journal of Functional and Logic Programming},
      volume={2000},
      number={1},
      publisher={The MIT Press},
      month={January},
      year={2000}
    }

----------------------------------------------------------------

*back to* Main page