@article{church-1932-spfl,
  author="A. Church",
  title="A Set of Postulates for the Foundations of Logic",
  journal="Annals of Mathematics",
  volume=33,
  pages="346--366",
  number=1,
  year=1932
}

@article{church-1933-spfl,
  author="A. Church",
  title="A Set of Postulates for the Foundations of Logic",
  journal="Annals of Mathematics",
  volume=34,
  pages="839--864",
  number=2,
  year=1933
}
  
@phdthesis{girard-1972-ifecaos,
  author="J.-Y. Girard",
  title="Interpr{\'e}tation Fonctionelle et {\'E}limination des "
       # "Coupures Dans l'Arithm{\'e}tique d'Ordre Sup{\'e}rieur",
  school="Universit{\'e} Paris 7",
  year=1972
}

@article{girard-1989-pt,
  author="J.-Y. Girard and Y. Lafont and P. Taylor",
  title="Proofs and Types",
  journal="Tracks in Theoretical Computer Science",
  year=1989
}

@inproceedings{reynolds-1974-ttts,
  author="John. C. Reynolds",
  title="Towards a Theory of Type Systems",
  booktitle="Lecture Notes in Computer Science",
  year=1974,
  editor="Ehring et al.",
  volume=19,
  pages="408--425",
  publisher="Springer-Verlag"
}

@article{boehm-1985-astlpta,
  author="C. B{\"o}hm and A. Bernarducci",
  title="Automatic Synthesis of Typed $\lambda$-Programs on Term "
       # "Algebras",
  journal="Theoretical Computer Science",
  volume=39,
  number="2--3",
  pages="135--154",
  month=aug,
  year=1985
}

@phdthesis{paulin-1989-epscc,
  author="C. Paulin-Mohring",
  title="Extraction de Programmes Dans le Calcul des Constructions",
  month=jan,
  school="Universit{\'e} Paris 7",
  year=1989,
  url="http://www.lri.fr/~paulin/these.ps.gz"
}

@inproceedings{pfenning-1990-pmfps,
  author="F. Pfenning and C. Paulin-Mohring",
  booktitle="Proceedings of Mathematical Foundations of "
           # "Programming Semantics",
  note="technical report CMU-CS-89-209",
  publisher="Springer-Verlag",
  address = "Berlin",
  series="Lecture Notes in Computer Science",
  volume=442,
  title="Inductively defined types in the Calculus of Constructions",
  year=1990
}

@incollection{paulin-1993-iddcrp,
  author= "Christine Paulin-Mohring",
  title = "Inductive Definitions in the System {Coq}: Rules and Properties",
  booktitle = "Proceedings of the 1st Int.\ Conf.\ on Typed Lambda Calculi "
           # "and Applications, {TLCA}'93, Utrecht, The Netherlands, "
	   # "16--18 March 1993",
  volume = 664,
  publisher = "Springer-Verlag",
  address = "Berlin",
  editor = "M. Bezem and J. F. Groote",
  pages = "328--345",
  year = 1993,
  url = "citeseer.nj.nec.com/paulin-mohring92inductive.html"
}

@InProceedings{shao-2002-tscb,
  author = 	 "Z. Shao and B. Saha and V. Trifonov and N. Papaspyrou",
  title = 	 "A Type System for Certified Binaries",
  booktitle = 	 "Proceedings of the 29th Annual Symposium on Principles of "
               # "Programming Languages (POPL 2002)",
  year =	 2002,
  pages =	 "217--232",
  address =	 "Portland, OR, USA",
  month =	 jan
}

@InProceedings{sellink-1994-vpaptt,
  author = 	 "M. P. A. Sellink",
  title = 	 "Verifying process algebra proofs in type theory",
  booktitle = 	 "Proceedings of the International Workshop on Semantics "
               # " of Specipication Languages (SOSL 1993)",
  year =	 1994,
  editor =	"D. J. Andrews and J. F. Groote and C. A. Middelburg",
  publisher = 	"Springer"
}

@inproceedings{necula-1997-pcc,
  author="G. Necula",
  title="Proof-Carrying Code",
  booktitle="Proceedings of the 24th Annual Symposium on Principles of "
           # "Programming Languages (POPL 1997)",
  pages="106--119",
  publisher="ACM Press",
  address="New York",
  year=1997,
  month=jan
}

@inproceedings{necula-1996-skertc,
  author="G. Necula and P. Lee",
  title="Safe Kernel Extensions without Run-Time Checking",
  booktitle="Proceedings of the 2nd USENIX Symposium on Operating "
	# "System Design and Implementation", 
  year="1996",
  publisher="USENIX Association",
  pages="229--243"
}

@phdthesis{necula-1998-cp,
  title = "Compiling with Proofs",
  author = "G. Necula",
  school = "Carnegie Mellon University",
  year = 1998,
  month=sep,
  number = "CMU-CS-98-154"
}

@inproceedings{appel-2000-smtmipcc,
  author="Andrew W. Appel and Amy P. Felty",
  title="A Semantic Model of Types and Machine Instructions for "
	# "Proof-Carrying Code",
  booktitle="Proceedings of the 27th Annual Symposium on Principles of "
           # "Programming Languages (POPL 2000)",
  year=2000,
  publisher = "ACM Press",
  pages="243--253"
}

@InProceedings{appel-2001-fpcc,
  author = 	 "A. W. Appel",
  title = 	 "Foundational Proof-Carrying Code",
  booktitle = 	 "Proceedings of the 16th Annual IEEE Symposium on "
	       # "Logic in Computer Science",
  pages =	 "247--258",
  year =	 2001,
  month =	 jun
}

@inproceedings{harper-1995-cpita,
  author="Robert Harper and Greg Morrisett",
  title="Compiling Polymorphism Using Intensional Type Analysis",
  booktitle="Proceedings of the 22nd Annual Symposium on Principles of "
           # "Programming Languages (POPL 1995)",
  publisher="ACM Press",
  year="1995",
  pages="130--141"
}

@inproceedings{morrisett-1998-sftal,
  author="Greg Morrisett and David Walker and Karl Crary and Neal Glew",
  title="From {S}ystem {F} to Typed Assembly Language",
  booktitle="Proceedings of the 25th Annual Symposium on Principles of "
           # "Programming Languages (POPL 1998)",
  pages="85--97",
  publisher="ACM Press",
  year=1998,
  month=jan
}