Abstract data type

  1. A type-theoretic account of abstraction functions and cost verification
    Modular verification in dependent type theory using abstraction functions as types, with support for cost analysis and behavior verification while maintaining privacy guarantees.