The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
From MaRDI portal
Publication:5111301
DOI10.4230/LIPIcs.FSCD.2017.6zbMath1434.68213OpenAlexW2757364446MaRDI QIDQ5111301
Publication date: 26 May 2020
Full work available at URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.6
strong normalizationsum typereducibility methodrestricted reducibility theoremtype-directed expansion
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
- Developing developments
- Exact bounds for lengths of reductions in typed λ-calculus
- A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
- Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
- Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- Polymorphic higher-order recursive path orderings
- Computability Closure: Ten Years Later
- Extensional Rewriting with Sums
- Retraction map categories and their applications to the construction of lambda calculus models
- Categorical data types in parametric polymorphism
- Simulating expansions without expansions
- Why commutative diagrams coincide with equivalent proofs
- The virtues of eta-expansion
- From programming-by-example to proving-by-example
- Triangulation in rewriting
- A syntactic approach to eta equality in type theory
- On equivalence and canonical forms in the LF type theory
- Deciding equivalence with sums and the empty type
- The exp-log normal form of types: decomposing extensional equality and representing terms compactly
- On the Church-Rosser property for the direct sum of term rewriting systems
- Inductive-data-type systems
