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

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

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