Congruence types

DOI10.1007/3-540-61377-3_30MaRDI QIDQ6560160zbMATH OpenFDO

Authors Gilles Barthe, Herman Geuvers

Publication date 21 June 2024

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic in computer science (03B70) Type theory (03B38)

Recommendations

• Algebraic semantics of rewriting terms and types
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS
• Modular properties of algebraic type systems
• Pure patterns type systems
• Polymorphic rewriting conserves algebraic confluence

Cites work

• scientific article; zbMATH DE number 4096759 (Why is no real title available?)
• scientific article; zbMATH DE number 4096760 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 108434 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• A short and flexible proof of strong normalization for the calculus of constructions
• A two-level approach towards lean proof-checking
• Typed lambda calculi and applications. 2nd international conference, TLCA '95, Edinburgh, GB, April 10--12, 1995. Proceedings

This page was built for publication: Congruence types

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