HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Metatheoretic Results for a Modal Lambda Calculus

Pierre Leleu 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
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 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 usual contexts. This latter peculiarity leads to the main difficulties and consequently to the main original features in our proofs. Since the original proof was extended to an inductive setting, we expect our proof could also be extended to a calculus with higher order abstract syntax and induction.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 12:33:16 PM
Last modification on : Friday, February 4, 2022 - 3:16:13 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:42:34 PM


  • HAL Id : inria-00073328, version 1



Pierre Leleu. Metatheoretic Results for a Modal Lambda Calculus. RR-3361, INRIA. 1998. ⟨inria-00073328⟩



Record views


Files downloads