The lambda sigma calculus and strong normalization

Anders Schack-Nielsen, Carsten Schürmann

Research output: Book / Anthology / Report / Ph.D. thesisReportResearch


Explicit substitution calculi can be classified into several dis- tinct categories depending on whether they are confluent, meta-confluent, strong normalization preserving, strongly normalizing, simulating, fully compositional, and/or local. In this paper we present a variant of the λσ-calculus, which satisfies all seven conditions. In particular, we show how to circumvent Mellies counter-example to strong normalization by a slight restriction of the congruence rules. The calculus is implemented as the core data structure of the Celf logical framework. All meta-theoretic aspects of this work have been mechanized in the Abella proof assistant.
Original languageEnglish
PublisherIT-Universitetet i København
Number of pages13
ISBN (Print) 978-87-7949-249-3
Publication statusPublished - 2011


  • Explicit Substitution Calculi
  • Confluence
  • Strong Normalization
  • λσ-calculus
  • Proof Assistant (Abella)


Dive into the research topics of 'The lambda sigma calculus and strong normalization'. Together they form a unique fingerprint.

Cite this