Q5111301 (Q5111301): Difference between revisions

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