The λσ-Calculus and Strong Normalization

TR-2010-132, Author: Anders Schack-Nielsen

The λσ-Calculus and Strong Normalization

Anders Schack-Nielsen

October 2010

Abstract

The general λσ-calculus is not strongly normalizing, but we show how a small restriction in the reduction rules allows us to prove strong normalization.

The proof has been formalized in the proof assistant Abella.

Technical report [TR-2010-132] in IT University Technical Report Series, October 2010.

Available as PDF.