Type theory and rewriting
Fr\'ed\'eric Blanqui (LRI)
TL;DR
This paper investigates the properties of dependent type systems in lambda calculus and rewriting, focusing on aspects like termination to ensure soundness and reliability.
Contribution
It provides new insights into the termination properties of dependent types within lambda calculus and rewriting frameworks.
Findings
Established conditions for termination in dependent type systems
Analyzed the impact of rewriting on type system properties
Proposed methods to ensure soundness in type-theoretic frameworks
Abstract
We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.
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