The confluent terminating context-free substitutive rewriting system for the lambda-calculus with surjective pairing & terminal type

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo, inspired by Knuth-Bendix completion, introduced a confluent rewriting system of the naive rewriting system. Their system is a confluent (CR) rewriting system stable under contexts. They left the strong normalization (SN) of their rewriting system open. By Girard's reducibility method with restricting reducibility theorem, we prove SN of their rewriting, and SN of the extensions by polymorphism and (terminal types caused by parametric polymorphism). We extend their system by sum types and eta-like reductions, and prove the SN. We compare their system to type-directed expansions.

Original languageEnglish
Title of host publication2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
EditorsDale Miller
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770477
DOIs
Publication statusPublished - 2017 Sep 1
Event2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 - Oxford, United Kingdom
Duration: 2017 Sep 32017 Sep 9

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume84
ISSN (Print)1868-8969

Other

Other2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
CountryUnited Kingdom
CityOxford
Period17/9/317/9/9

Keywords

  • Reducibility method
  • Restricted reducibility theorem
  • Strong normalization
  • Sum type
  • Typedirected expansion

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'The confluent terminating context-free substitutive rewriting system for the lambda-calculus with surjective pairing & terminal type'. Together they form a unique fingerprint.

Cite this