@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 }