Showing cs.PLShow all
2 papers · 1 filter
cs.PL2025
Coverage Semantics for Dependent Pattern Matching
Joseph Eremondi, Ohad Kammar
Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching…
cs.PL2023
Strictly Monotone Brouwer Trees for Well-founded Recursion Over Multiple Arguments
Joseph Eremondi
Ordinals can help prove termination for dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data stru…