@inproceedings{crary+:mafcc-cade,
  author    = {Karl Crary and
               Susmit Sarkar},
  title     = {Foundational Certified Code in a Metalogical Framework},
  booktitle = {International Conference on Automated Deduction},
  year      = {2003},
  pages     = {106-120},
  series    = {Lecture Notes in Computer Science},
  volume    = {2741},
  isbn      = {3-540-40559-3},
}