Congruence types

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

Authors Gilles Barthe, Herman Geuvers

Publication date 21 June 2024

Full work available at URL https://doi.org/10.1007/3-540-61377-3_30

Mathematics Subject Classification ID

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

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

• A short and flexible proof of strong normalization for the calculus of constructions
• A two-level approach towards lean proof-checking
• 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?)
• 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)