test.bib 5.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187
@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
188
}