Inductive-data-type systems
From MaRDI portal
Recommendations
Cites work
- A logic programming language with lambda-abstraction, function variables, and simple unification
- Abstract data type systems
- Combinators, \(\lambda\)-terms and proof theory
- Combinatory reduction systems: Introduction and survey
- Higher-order rewrite systems and their confluence
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- scientific article; zbMATH DE number 3928956 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 4124996 (Why is no real title available?)
- scientific article; zbMATH DE number 1255555 (Why is no real title available?)
- scientific article; zbMATH DE number 512772 (Why is no real title available?)
- scientific article; zbMATH DE number 683368 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1373518 (Why is no real title available?)
- scientific article; zbMATH DE number 1405632 (Why is no real title available?)
- scientific article; zbMATH DE number 3331288 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- Intensional interpretations of functionals of finite type I
- Linear unification of higher-order patterns
- Modularity of strong normalization in the algebraic-λ-cube
- Polymorphic rewriting conserves algebraic strong normalization
- Specification and proof in membership equational logic
Cited in
(22)- Inductive data types for predicate transformers
- Abstract data type systems
- Corrigendum to: ``Inductive-data-type systems
- Expression reduction systems with patterns
- Semantic foundations for generalized rewrite theories
- Normal higher-order termination
- The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics
- Strong normalisation in two Pure Pattern Type Systems
- The Computability Path Ordering: The End of a Quest
- Size-based termination of higher-order rewriting
- Termination checking with types
- Remarks on isomorphisms of simple inductive types
- scientific article; zbMATH DE number 7450013 (Why is no real title available?)
- Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
- scientific article; zbMATH DE number 7566074 (Why is no real title available?)
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
- Wanda -- a higher-order termination tool (system description)
- Higher-order constrained dependency pairs for (universal) computability
- Paradoxical connectives: proof-theoretic semantics, recursion, and fixed-point operators
- Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
- An initial algebra approach to term rewriting systems with variable binders
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
This page was built for publication: Inductive-data-type systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5958292)
