The λμT-calculus

Herman Geuvers, Robbert Krebbers, James McKinna

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand control operators, one should also include these in the calculus. As a first step in that direction, we introduce , a combination of Parigotʼs λμ-calculus and Gödelʼs T, to extend a calculus with control operators with a datatype of natural numbers with a primitive recursor.

We consider the problem of confluence on raw terms, and that of strong normalization for the well-typed terms. Observing some problems with extending the proofs of Baba et al. and Parigotʼs original confluence proof, we provide new, and improved, proofs of confluence (by complete developments) and strong normalization (by reducibility and a postponement argument) for our system.

We conclude with some remarks about extensions, choices, and prospects for an improved presentation.
Original languageEnglish
Pages (from-to)676-701
Number of pages26
JournalAnnals of Pure and Applied Logic
Volume164
Issue number6
DOIs
Publication statusPublished - Jun 2013

Fingerprint Dive into the research topics of 'The λμT-calculus'. Together they form a unique fingerprint.

  • Cite this