감가 분석(Amortized analysis)은 물리학자의 관점에서 프레임화될 수 있으며, 잠재 함수(potential functions)를 사용하여 의존 타입 이론(dependent type theory)에서 수동 검증이 가능하고, 은행가의 관점에서는 타입 레벨 크레딧 주석(type-level credit annotations)을 사용하여 하위 구조 타입 이론(substructural type theory)에서 자동 추론이 가능합니다. 본 연구에서는 이러한 관점들을 Calf라는 의존 타입 이론 비용 검증 시스템에 통합합니다. 물리학자의 관점에서, 우리는 모든 타입을 추상화 함수(abstraction function)와 잠재 함수의 융합으로 구성된다는 파쇄 및 접합 정리(fracture and gluing theorem)를 제시합니다. 구축에 따라, 두 그러한 타입 사이의 모든 프로그램은 동작의 모듈성(modularity of behavior)을 용이하게 하기 위해 추상화를 보존해야 하며, 비용의 모듈성을 용이하게 하기 위해 잠재량을 보존해야 합니다. 은행가의 관점을 통합하여, 우리는 크레딧과 디빗에 대한 타입 연산자들을 합성적으로 구성합니다. 그런 다음, 우리는 크레딧과 디빗을 사용한 프로그래밍을 위한 계층적 하위 구조 의존 타입 이론인 Giralf를 정의하며, 이는 Calf의 하위 언어로 의미론적으로 해석됩니다. 마지막으로, 우리는 추론 알고리즘을 조정하여 제한된 클래스의 Calf 프로그램을 Giralf 대응물로 변환함으로써, Calf 내 일반적인 알고리즘들의 비용 분석을 자동화합니다.