scientific article; zbMATH DE number 4126684

MaRDI QIDQ4206388zbMATH OpenFDO

Authors David Basin

Publication date 1990

zbMATH Keywords

constructive type theoryNuprlterm rewriting systems

Mathematics Subject Classification ID

Thue and Post systems, etc. (03D03) Abstract data types; algebraic specification (68Q65) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 827981
• A new look at generalized rewriting in type theory
• scientific article; zbMATH DE number 2003149
• A Rewriting Semantics for Type Inference
• Modelling general recursion in type theory
• scientific article; zbMATH DE number 2038715
• Type Reconstruction for General Refinement Types
• A Rewriting Logic Approach to Type Inference
• Algebraic semantics of rewriting terms and types
• Generalization from partial parametrization in higher-order type theory

Cited in

(13)

• Rewrite systems on a lattice of types
• A rewrite-based type discipline for a subset of computer algebra
• Type introduction for equational rewriting
• A new look at generalized rewriting in type theory
• scientific article; zbMATH DE number 1498422 (Why is no real title available?)
• Generalizing Def and Pos to Type Analysis
• scientific article; zbMATH DE number 827981 (Why is no real title available?)
• Introduction to generalized type systems
• (Head-)normalization of typeable rewrite systems
• Term Rewriting and Applications
• Algebraic semantics of rewriting terms and types
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• A mechanically assisted constructive proof in category theory

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication:

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