We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using B oogie and prove a suite of data structure manipulating programs correct.

@article{MuraliRM24,
  title = {Predictable Verification using Intrinsic Definitions},
  author = {Adithya Murali and Cody Rivera and P. Madhusudan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {PLDI},
  year = {2024},
  doi = {10.1145/3656450}
}