research
∙
10/26/2022
Higher-Order MSL Horn Constraints
The monadic shallow linear (MSL) class is a decidable fragment of first-...
share
research
∙
11/24/2021
CycleQ: An Efficient Basis for Cyclic Equational Reasoning
We propose a new cyclic proof system for automated, equational reasoning...
research
∙
08/04/2020
Intensional Datatype Refinement
The pattern-match safety problem is to verify that a given functional pr...
research
∙
07/26/2016