Rewriting Modulo \beta in the \lambda\Pi-Calculus Modulo
Ronan Saillard (MINES ParisTech, PSL Research University, France)

TL;DR
This paper introduces rewriting modulo beta in the lambda-Pi-calculus Modulo, ensuring key logical properties under broader conditions by encoding it into Higher-Order Rewrite Systems.
Contribution
It extends the lambda-Pi-calculus Modulo with a notion of rewriting modulo beta, enabling confluence and logical properties without requiring full confluence of the combined system.
Findings
Rewriting modulo beta ensures subject reduction and uniqueness of types.
Encoding into Higher-Order Rewrite Systems allows leveraging existing confluence results.
The approach broadens the applicability of the lambda-Pi-calculus Modulo in logical frameworks.
Abstract
The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type systems in a shallow way. Basic properties such as subject reduction or uniqueness of types do not hold in general in the lambda-Pi-calculus Modulo. However, they hold if the rewrite system generated by the rewrite rules together with beta-reduction is confluent. But this is too restrictive. To handle the case where non confluence comes from the interference between the beta-reduction and rewrite rules with lambda-abstraction on their left-hand side, we introduce a notion of rewriting modulo beta for the lambda-Pi-calculus Modulo. We prove that confluence of rewriting modulo beta is enough to ensure subject reduction and uniqueness of types. We achieve…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
