A Modal Lambda Calculus with Iteration and Case Constructs

Pierre Leleu 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : An extension of the simply-typed $\lambda$-calculus allowing iteration and casereasoning over terms defined by means of higher order abstract syntax has recently been introduced by Joëlle Despeyroux, Frank Pfenning and Carsten Schürmann. This thorny mixing is achieved thanks to the help of the operator `$\Bf modal logic IS4. Here we give a new presentation of their system, with reduction rules, instead of evaluation judgments, that compute the canonical forms of terms. Our presentation is based on a modal $\lambda$-calcu- lus that is better from the user's point of view, is more concise and we do not impose a particular strategy of reduction during the computation. Our system enjoys the decidability of typability, soundness of typed reduction with respect to typing rules, the Church-Rosser and strong normalization properties. Finally itis a conservative extension of the simply-typed $\lambda$-calculus.
Type de document :
Rapport
RR-3322, INRIA. 1997
Liste complète des métadonnées

https://hal.inria.fr/inria-00073367
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:38:12
Dernière modification le : samedi 27 janvier 2018 - 01:30:56
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:52:20

Fichiers

Identifiants

  • HAL Id : inria-00073367, version 1

Collections

Citation

Pierre Leleu. A Modal Lambda Calculus with Iteration and Case Constructs. RR-3322, INRIA. 1997. 〈inria-00073367〉

Partager

Métriques

Consultations de la notice

194

Téléchargements de fichiers

172