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

Authors 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)

Recommendations

• scientific article; zbMATH DE number 176742
• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• Adding algebraic rewriting to the untyped lambda calculus

Cites work

• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 48365 (Why is no real title available?)
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 3573844 (Why is no real title available?)
• scientific article; zbMATH DE number 1231495 (Why is no real title available?)
• scientific article; zbMATH DE number 512797 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 3328152 (Why is no real title available?)
• A modular type-checking algorithm for type theory with singleton types and proof irrelevance
• A syntactic approach to eta equality in type theory
• Categorical data types in parametric polymorphism
• Computability Closure: Ten Years Later
• Deciding equivalence with sums and the empty type
• Developing developments
• Exact bounds for lengths of reductions in typed \(\lambda\)-calculus
• Extensional Rewriting with Sums
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• From programming-by-example to proving-by-example
• Harnessing first order termination provers using higher order dependency pairs
• Inductive-data-type systems
• On equivalence and canonical forms in the LF type theory
• On the Church-Rosser property for the direct sum of term rewriting systems
• Polymorphic higher-order recursive path orderings
• Retraction map categories and their applications to the construction of lambda calculus models
• Simulating expansions without expansions
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• The exp-log normal form of types: decomposing extensional equality and representing terms compactly
• The virtues of eta-expansion
• Triangulation in rewriting
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• Why commutative diagrams coincide with equivalent proofs

Cited in

(3)

• Proof of termination of the rewriting system SUBSET on CCL
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• A confluent reduction for the λ-calculus with surjective pairing and terminal object

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)