Approximation and normalization results for typeable term rewriting systems

DOI10.1007/3-540-61254-8_17MaRDI QIDQ4645802zbMATH OpenOpenAlexFDO

Authors Steffen Van Bakel, Maribel Fernández

Publication date 11 January 2019

Published in Higher-Order Algebra, Logic, and Term Rewriting (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61254-8_17

zbMATH Keywords

normal formapproximation theoremtype assignmentfunction symboltypeable term

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Recommendations

• Normalization results for typeable rewrite systems
• (Head-)normalization of typeable rewrite systems
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS
• Normalization, approximation, and semantics for combinator systems
• scientific article; zbMATH DE number 512770

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 512770 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1479633 (Why is no real title available?)
• scientific article; zbMATH DE number 883895 (Why is no real title available?)
• (Head-)normalization of typeable rewrite systems
• A filter lambda model and the completeness of type assignment
• An extension of basic functionality theory for -calculus
• Combinatory logic. With two sections by William Craig.
• Complete restrictions of the intersection type discipline
• Full abstraction and limiting completeness in equational languages
• Intensional interpretations of functionals of finite type I
• Intersection types for combinatory logic
• Meaningless terms in rewriting
• Principal Type Schemes for the Strict Type Assignment System
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Typing and computational properties of lambda expressions

Cited in

(9)

• Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation
• Normalization properties for shallow TRS and innermost rewriting
• The heart of intersection type assignment: Normalisation proofs revisited
• Term rewriting for normalization by evaluation.
• Normalization, approximation, and semantics for combinator systems
• A rewriting view of simple typing
• (Head-)normalization of typeable rewrite systems
• Strongly normalising cut-elimination with strict intersection types
• Normalization results for typeable rewrite systems

This page was built for publication: Approximation and normalization results for typeable term rewriting systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4645802)