An indexed model of recursive types for foundational proof-carrying code

Andrew W. Appel, David A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, 23(5):657-683, 2001. [doi]

Abstract

Abstract is missing.