The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

DOI10.4230/LIPICS.FSCD.2017.6zbMATH Open1434.68213OpenAlexW2757364446MaRDI QIDQ5111301FDOQ5111301

Yohji Akama

Publication date: 26 May 2020

Full work available at URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.6

zbMATH Keywords

strong normalizationsum typereducibility methodrestricted reducibility theoremtype-directed expansion

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Cites Work

• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Polymorphic higher-order recursive path orderings
• Exact bounds for lengths of reductions in typed \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Developing developments
• Title not available (Why is that?)
• On the Church-Rosser property for the direct sum of term rewriting systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Categorical data types in parametric polymorphism
• Simulating expansions without expansions
• The virtues of eta-expansion
• From programming-by-example to proving-by-example
• Why commutative diagrams coincide with equivalent proofs
• Inductive-data-type systems
• Computability Closure: Ten Years Later
• Title not available (Why is that?)
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• Title not available (Why is that?)
• A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
• On equivalence and canonical forms in the LF type theory
• Retraction map categories and their applications to the construction of lambda calculus models
• Extensional Rewriting with Sums
• Deciding equivalence with sums and the empty type
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
• The exp-log normal form of types: decomposing extensional equality and representing terms compactly
• Triangulation in rewriting
• A syntactic approach to eta equality in type theory

Cited In (2)

• Title not available (Why is that?)
• A confluent reduction for the λ-calculus with surjective pairing and terminal object

   Recommendations

• Title not available (Why is that?) 👍 👎
• A confluent reduction for the λ-calculus with surjective pairing and terminal object 👍 👎
• A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object 👍 👎
• Adding algebraic rewriting to the untyped lambda calculus 👍 👎

This page was built for publication: The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111301)