%%
%%
%% BibTeX-file{
%%  author       = {Lars Birkedal}     
%%  date         = {June 1999}
%%  filename     = {realizability.bib}
%%  url          = {http://www.cs.cmu.edu/~birkedal/realizability.bib} 
%%  abstract     = {Bibiliography on Realizability}		  
%% }
%%
%% The BibTeX entries are formatted following the guidelines
%% for bibliography files in Hypatia, see
%%	http://www.hypatia.dcs.qmw.ac.uk/html/bibliography
%% 
%%
%% 
%%

@inproceedings{AbadiM:modprt, 
   author =   {M. Abadi and G.D. Plotkin},
   title =    {A per Model of Polymorphism and Recursive Types},
   pages =    {355-365},
   editor =   {J. Mitchell},
   booktitle = {5th Annual IEEE Symposium on Logic in Computer Science},
   address =  {Philadelphia},
   publisher= {IEEE Computer Society Press},
   year =     1990
}
		  
@book{AbadiM:theo,
  author = "M. Abadi and L. Cardelli",
  title = "A Theory of Objects",
  publisher = "Springer Verlag",
  Year = 1996
}

@Unpublished{AbramskyS:typrea,
  author = 	 {S. Abramsky},
  title = 	 {Typed Realizability},
  note = 	 {Talk at the workshop on Category Theory and Computer
		  Science in Cambridge, England}, 
  year =	 1995,
  month = 	 aug
}

@misc{AczelP:intiho,
  author="Aczel, P.H.G.",
  title="A note on interpreting intuitionistic higher-order
 	logic",
  year=1980,
  note="Handwritten note"
}

@phdthesis{AltenkirchT:conits,
  author = "T. Altenkirch",
  title = "Constructions, Inductive Types and Strong Normalization",
  year = 1993,
  school = "University of Edinburgh",
  note = "Available as report ECS-LFCS-93-279"
}
		  
@article{AmadioR:recor,
   author =  {R. Amadio},
   title =   {Recursion over Realizability Structures},
   journal = {Information and Computation},
   year =    1991,
   volume =  91,
   pages =   {55-85}
}
		  
@techreport{AspertiA:intmpl,
   author =      {A. Asperti},
   title =       {The Internal Model of Polymorphic Lambda Calculus},
   year =        1988,
   number =      {CMU-CS-88-155},
   institution = {Carnegie Mellon University}
}

@InProceedings{AvigadJ:reaica,
  author = 	 {J. Avigad},
  title = 	 {A realizability interpretation for classical
                  arithmetic},
  booktitle = 	 {Logic Colloquium '98},
  pages =	 {57--90},
  year =	 2000,
  editor =	 {Buss and H\'ajek and Pudl\'ak},
  number =	 13,
  series =	 {Lecture Notes in Logic},
  publisher =	 {AK Peters}
}
		  
@Unpublished{AwodeyS:locrtm,
  author = 	 {S.~Awodey and L.~Birkedal and D.S.~Scott},
  title = 	 {Local Realizability Toposes and a Modal Logic 
                  for Computability}, 
  note = 	 {Presented at \emph{Tutorial Workshop on 
                  Realizability Semantics, FLoC'99}, Trento, Italy 1999.},
  year = 	 1999
}
		  
@article{BainbridgeS:funp,
   author =  {S. Bainbridge and P.J. Freyd and A. Scedrov and P. Scott},
   title =   {Functorial Polymorphism},
   journal = {Theoretical Computer Science},
   year =    1990,
   volume =  70,
   pages =   {35-64}
}

@article{BarbaneraF:profcr,
  author="Barbanera, F. and Martini, S.",
  title="Proof--Functional Connectives and Realizability",
  journal="Archive for Mathematical Logic",
  volume=33,
  year=1994,
  pages="189--211"
}

@article{BarendregtHP:comlac,
  author="Barendregt, H.P.",
  title="Combinatory logic and the axiom of choice",
  journal="Indagationes Mathematicae",
  year=1973,
  volume=35,
  pages="203--221"
}
		  
@article{BarendregtHP:intgts,
  author       = {Barendregt, H.P.},
  title        = {Introduction to Generalized Type Systems},
  journal      = {Journal of Functional Programming},
  volume       =  1,
  number       =  2,
  year         =  1991,
  pages        = {125--154},
  source       = {ftp://src.doc.ic.ac.uk/computing/bibliographies/Karlsruhe/Compiler/Functional.bib/},
  source-date  = {Tue 26 Aug 97}}
		  
@inproceedings{BarrM:exac,
   author =   {M. Barr},
   title =    {Exact Categories},
   pages =    {1-120},
   editor =    {M. Barr and P.A. Grillet and D. Van Osdol},
   booktitle =     {Exact Categories and Categories of Sheaves},
   series =    {Lecture Notes in Mathematics},
   volume =    236,
   publisher = {Springer-Verlag},
   year =      1971
}
		  
@unpublished{BauerA:equs,
  author = 	 {A. Bauer and L. Birkedal and D.S. Scott},
  title = 	 {Equilogical Spaces},
  note = 	 {Submitted for publication},
  year =	 1998
}
		  
@article{BeesonM:chutcs,
  author="Beeson, M.J. and Scedrov, A.",
  title="Church's Thesis, Continuity and Set Theory",
  year=1984,
  journal={Journal of Symbolic Logic},
  volume=49,
  pages="630--643"
}
		  
@article{BeesonM:concif,
  author="Beeson, M.J.",
  title="Continuity and Comprehension in Intuitionistic Formal
	Systems",
  journal="Pacific Journal of Mathematics",
  volume=68,
  year=1977,
  pages="29--40"
}
		  
@inproceedings{BeesonM:conist,
  author="Beeson, M.J.",
  title="Continuity in Intuitionistic Set Theories",
  booktitle="Logic Colloquium '78",
  editor="Boffa, M. and van Dalen, D. and Mc{A}loon, K.",
  pages="1--52",
  year=1979,
  publisher={North-Holland Publishing Company}
}

@article{BeesonM:derrir,
  author="Beeson, M.J.",
  title="Derived Rules of Inference Related to the 
	Continuity of Effective Operations",
  year=1976,
  journal={Journal of Symbolic Logic},
  volume=41,
  pages="328--336",
  reviews="MR 54#7208; RZH 77.3A36; ZBL 333#02027"
}

@article{BeesonM:extccm,
  title="Extensionality and Choice in Constructive Mathematics",
  author="Beeson, M.J.",
  journal="Pacific Journal of Mathematics",
  volume=88,
  year=1980,
  pages="1--28"
}
		  
@inproceedings{BeesonM:forcm,
  author="Beeson, M.J.",
  title="Formalizing Constructive Mathematics: {W}hy and How?",
  booktitle="Constructive Mathematics",
  editor="Richman, F.",
  year=1981,
  publisher={Springer-Verlag},
  pages="146--190"
}
  
@book{BeesonM:foucm,
  author="Beeson, M.J.",
  title="Foundations of constructive mathematics",
  year=1985,
  publisher={Springer-Verlag},
  pages="xxiii+466pp",
  reviews="JSL 52.278; MR 86k:03055; RZH 85.9A14; ZBL 565#03028"
}
		  
@article{BeesonM:nonifs,
  author="Beeson, M.J.",
  title="The Nonderivability in Intuitionistic Formal 
	Systems of Theorems on the Continuity of 
	Effective Operations",
  year="1975",
  journal={Journal of Symbolic Logic},
  volume=41,
  pages="321--346",
  reviews="MR 51#10050; RZH 76.12A49; ZBL 316#02038"
}
		  
@article{BeesonM:pricc,
  author="Beeson, M.J.",
  title="Principles of continuous choice and continuity of
	functions in formal systems for constructive 
	mathematics",
  journal={Arhive for Mathematical Logic},
  year=1977,
  volume=12,
  pages="249--322"
}
		  
@article{BeesonM:recmcs,
  author="Beeson, M.J.",
  title="Recursive Models for Constructive Set Theories",
  year=1982,
  journal={Annals of Pure and Applied Logic},
  volume=23,
  pages="127--178",
  reviews="MR 85d:03111; ZBL 514#03039"
}
		
@article{BeesonM:unpifs,
  author="Beeson, M.J.",
  title="The Unprovability in Intuitionistic Formal Systems of 
         Continuity of Effective Operations on the Reals",
  year=1976,
  journal={Journal of Symbolic Logic},
  volume=41,
  pages="18--24",
  reviews="MR 54#2425; RZH 77.2A42; ZBL 333#02026"
}
		  
@article{BeesonM:goodmant,
  title="Goodman's Theorem and Beyond",
  author="Beeson, M.J.",
  journal="Pacific Journal of Mathematics",
  year=1979,
  volume=84,
  pages="1--28"
}
		  
@Unpublished{BenaissaZ:catamll,
  author = 	 "Z.E-L. Benaissa and E. Moggi and W. Taha and T. Sheard",
  title = 	 "A Categorical Analysis of Multi-Level Languages",
  note =	 "Manuscript",
  year =	 1999,
  month =	 jan
}
		  
@TechReport{BentonPN:mixlnl,
  author = 	 {P.N. Benton},
  title = 	 {A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Preliminary Report)},
  institution =  {University of Cambridge},
  year = 	 {1995}
}
		  
@techreport{BerardiS:comcax,
  author="Berardi, S. and Bezem, M.A. and Coquand, T.",
  title="On the Computational Content of the Axiom of Choice",
  year=1994,
  number="Logic Group Preprint Series, 116",
  institution="Department of Philosophy, Utrecht University"	
}
		  
@inproceedings{BergerU:proecp,
  author="Berger, U. and Schwichtenberg, H.",
  title="Program Extraction from Classical Proofs",
  booktitle="Logic and Computational Complexity.
	International Workshop LCC '94, Indianapolis, IN,
	USA, October 1994",
  editor="Leivant, D.",
  year=1995,
  publisher={Springer-Verlag},
  pages="77-97",
  volume=960,
  series="Lecture Notes in Computer Science"
}
		  
@misc{BergerU:propms,
  author="Berger, U. and Schwichtenberg, H. and Seisenberger, M.",
  title="From Proofs to Programs in the {Minlog} System.
	{T}he {W}arshall algorithm and {H}igman's lemma",
  year=1997,
  note="To appear in {\it Journal of Automated Reasoning}"
}

@phdthesis{BethkeI:npca,
  author = {I. Bethke},
  title = {Notes on Partial Combinatory Algebras},
  school = {Universiteit van Amsterdam},
  year = 1988 
}
		  
@phdthesis{BezemM:barrff,
  author="Bezem, M.",
  title="Bar Recursion and Functionals of Finite Type",
  year=1986,
  school="Rijksuniversiteit Utrecht"
}
		  
@article{BezemM:commff,
  author="Bezem, M.",
  title="Compact and Majorizable Functionals of Finite Type",
  journal={Journal of Symbolic Logic},
  pages="271--280",
  year=1989,
  volume=54
}
		  

@article{BezemM:majfft,
  author="Bezem, M.",
  title="Strongly Majorizable Functionals of Finite Type: 
	a Model for Bar Recursion Containing Discontinuous 
	Functionals",
  journal={Journal of Symbolic Logic},
  year=1985,
  volume=50,
  pages="652--660"
}

@PhdThesis{BirkedalL:devttc,
  author = 	 {L. Birkedal},
  title = 	 {Developing Theories of Types and Computability},
  school = 	 {School of Computer Science, Carnegie Mellon University},
  year = 	 1999,
  month =	 dec
}
		  
@inproceedings{BirkedalL:ttec,
  author = 	 {L. Birkedal and A. Carboni and G. Rosolini and D.S. Scott},
  title = 	 {Type Theory via Exact Categories},
  booktitle = 	 {Proceedings of the 13th Annual IEEE Symposium on Logic in
		  Computer Science},  
  year =	 1998,
  publisher = {IEEE Computer Society Press},
  address =	 {Indianapolis, Indiana},
  month =	 jun,
  pages =	 {188--198}
}
		  
@inproceedings{BruceK:permod,
  author="Bruce, K. and Mitchell, J.C.",
  title="PER models of subtyping, recursive types and higher-order polymorphism",
  year=1992,
  booktitle={Proc.\ 19th ACM Symp.\ on Principles of Programming},
  pages="316--327"
  }
		  
@book{BuchholzW:iteids,
  author="Buchholz, W. and Feferman, S. and Pohlers, W. and Sieg, W.",
  title="Iterated Inductive Definitions and Subsystems of
	Analysis: Recent Proof-Theoretical Studies",
  year=1981,
  publisher={Springer-Verlag},
}
		  
@inproceedings{BussS:polhiba,
  author="Buss, S.",
  title="The Polynomial Hierarchy and Intuitionistic Bounded
			Arithmetic",
  booktitle="Structure in Complexity Theory",
  publisher={Springer-Verlag},
  year=1986,
  pages="77-103",
  series="Springer Lecture Notes in Computer Science",
  volume=223		  
}
		  
@inproceedings{CarboniA:catarp,
   author =   {A. Carboni and P.J. Freyd and A. Scedrov},
   title =    {A Categorical Approach to Realizability 
	       and Polymorphic Types},
   pages =    {23-42},
   editor =   {M. Main and A. Melton and M. Mislove and D.Schmidt},
   booktitle ={Mathematical Foundations of Programming Language 
               Semantics},
   address =  {New Orleans},
   series =   {Lectures Notes in Computer Science},
   volume =   298,
   publisher ={Springer-Verlag},
   year =     1988
}

@article{CarboniA:freecl,
   author =  {A. Carboni and R. Celia Magno},
   title =   {The Free Exact Category on a Left Exact one},
   journal = {Journal of Australian Mathematical Society},
   volume = 33,
   year =    1982,
   number =  {A},
   pages =   {295-301}
}
	  
@misc{CarboniA:lccec,
  author = 	 {A. Carboni and G. Rosolini},
  title = 	 {Locally Cartesian Closed Exact Completions},
  journal = 	 {Journal of Pure and Applied Algebra},
  year = 	 {1998},
  OPTvolume = 	 {},
  note =	 {to appear}
}
		  
@article{CarboniA:regec,
  author =	 {A. Carboni and E.M. Vitale},
  title =	 {Regular and Exact Completions},
  year =	 {1998},
  volume =	 125,
  journal =	 {Journal of Pure and Applied Algebra},
  pages =        {79-117}
}

@article{CarboniA:somfcr,
   author =  {A. Carboni},
   title =   {Some Free Constructions in Realizability and Proof Theory},
   journal = {Journal of Pure and Applied Algebra},
   volume = 103,
   year =    1995,
   pages =   {117-148}
}
		  
@techreport{CardelliL:sembq,
   author =      {L. Cardelli and G. Longo},
   title =       {A Semantic Basis for {Q}uest},
   year =        1989,
   number =      55,
   institution = {Digital Equipment Corporation}
}

@article{CellucciC:opebrf,
  author="Cellucci, C.",
  title="Operazioni di {B}rouwer e Realizzabilita Formalizzata 
			({E}nglish Summary)",
  year=1971,
  journal="Annali della Scuola Normale Superiore di Pisa. Classe
          di Science. Fisiche e Matiche, Seria III",
  volume=25,
  pages="649--682",
  reviews="MR 51#12485; RZH 72.10A47; ZBL 242#02037"
}

		  
@article{CookS:funifc,
  author="Cook, S. and Urquhart, A.",
  title="Functional Interpretations of Feasibly Constructive Arithmetic",
  year=1993,
  journal={Annals of Pure and Applied Logic},
  volume=63,
  pages="103-200"
}
		  
@article{CoquandT:coc,
  author = "Th. Coquand and G. Huet",
  title = "The Calculus of Constructions",
  journal = "Information and Computation",
  year = "1988",
  volume = 76
}
		  
@article{CoquandT:domtmp,
   author =  {T. Coquand and C. Gunter and G. Winskel},
   title =   {Domain Theoretic Models of Polymorphism},
   journal = {Information and Computation},
   year =    1989,
   volume =  81,
   pages =   {123-167}
}
		  
@phdthesis{CoquandT:thec,
  author = "Th. Coquand",
  title = "Une Theorie des Constructions",
  school = "University of Paris VII",
  year = 1985
}
		  
@book{CutlandNJ:comp,
  author = {N.J. Cutland},
  title = {Computability},
  publisher = {Cambridge University Press},
  year = 1980
}
		  
@misc{DamnjanovicZ:elerea,
  author="Damnjanovic, Z.",
  title="Elementary Realizability",
  year=1996,
  note="Submitted to {\it Journal of Philosophical Logic}"
}
		  
@article{DamnjanovicZ:minria,
  author="Damnjanovic, Z.",
  title="Minimal Realizability of Intuitionistic Arithmetic and
			Elementary Analysis",
  journal={Journal of Symbolic Logic},
  volume=60,
  year=1995,
  pages="1208--1241"
}
		  
@article{DamnjanovicZ:strprrI,
  author="Damnjanovic, Z.",
  title="Strictly Primitive Recursive Realizability, {I}",
  journal={Journal of Symbolic Logic},
  volume=59,
  year=1994,
  pages="1210--1227"
}
@inproceedings{DeJonghD:chaipc,
  author="de Jongh, D.H.J.",
  title="A Characterization of the Intuitionistic Propositional
			Calculus",
  year=1970,
  booktitle="Intuitionism and Proof Theory",
  editor="Kino, A. and Myhill, J. R. and Vesley, R. E.",
  publisher={North-Holland Publishing Company},
  pages="211--217"
}
		  
@inproceedings{DeJonghD:foropv,
  author="de Jongh, D.H.J.",
  title="Formulas of One Propositional Variable in Intuitionistic
			Arithmetic",
  booktitle="The L. E. J. Brouwer Centenary Symposium",
  editor="Troelstra, A. S. and van~Dalen, D.",
  year=1980,
  publisher={North-Holland Publishing Company},
  pages="51--64"
}
		  
@phdthesis{DeJonghD:invipc,
  author="de Jongh, D.H.J.",
  title="Investigations of the Intuitionistic Propositional
			Calculus",
  school="University of Wisconsin, Madison",
  year=1968
}
		  
@misc{DeJonghD:maxipc,
  title = "The maximality of the Intuitionistic Predicate Calculus
          with respect to Heyting's Arithmetic",
  author = "de Jongh, D.H.J.",
  note  = "typed manuscript from University of Winsconsin, Madison",
  year  = 1969
}

@article{DillerJ:diaiha,
  author="Diller, J. and Nahm, W.",
  title="Eine {V}ariante zur {D}ialectica--{I}nterpretation der 
	{H}eyting--{A}rithmetik endlicher {T}ypen",
  year=1974,
  journal={Archiv},
  volume=16,
  pages="49--66",
  reviews="MR 51#2873; RZH 74.10A125; ZBL 277#02006"
}
		  
@article{DillerJ:funiha,
  author="Diller, J.",
  title="Functional Interpretations of {H}eyting's Arithmetic in
	all Finite Types",
  journal="Nieuw Archief voor Wiskunde. Derde Serie",
  year=1979,
  volume=27,
  pages="70--97"
}
		  
@incollection{DillerJ:modrft,
  author="Diller, J.",
  title="Modified Realization and the 
			Formulae--as--Types Notion",
  year=1980,
  booktitle="To {H.B. Curry}: Essays on Combinatory Logic,
			Lambda Calculus and Formalism",
  publisher="Academic Press, New York",
  editor="Seldin, J. P. and Hindley, J. R.",
  pages="491--501",
  reviews="MR 82g:03093; ZBL 469#03006"
}
		  
@incollection{DragalinA:algimr,
  author="Dragalin, A.G.",
  title="An Algebraic Approach to Intuitionistic Models 
	of the Realizability Type ({R}ussian)",
  year=1979,
  booktitle="Issledovaniya po Neklassicheskim Logikam i Teorii Mnozhestv
(Investigations on Non-Classical Logics and Set Theory)",
  editor="Mikhajlov, A. I. et.al.",
  publisher="Nauka, Moskva",
  pages="83--201",
  reviews="MR 82a:03057; RZH 80.7A24; ZBL 427#03050"
}

@article{DragalinA:comprt,
  author="Dragalin, A.G.",
  title="The Computability of Primitive Recursive Terms 
	of Finite Type, and Primitive Recursive 
	Realization ({R}ussian)",
  year=1968,
  journal="Zapiski",
  volume=8,
  pages="32--45",
  reviews="MR 43#45; ZBL 176.279",
  note="Translation {\em Seminars in Mathematics. V.A.Steklov
			Mathematical Institute Leningrad} 
			8(1970), pp. 13--18. 
			This volume appeared as: A.O. Slisenko
			(ed.), {\em Studies in Constructive Mathematics and
			Mathematical Logic. Part II}. Consultants Bureau, 
			New York, London"
}
 
@book{DragalinA:matint,
  author="Dragalin, A.G.",
  title="Mathematical Intuitionism",
  year="1988",
  publisher={American Mathematical Society},
  note="Translation of the {R}ussian original from 1979"
}

@article{DragalinA:reamar,
  author="Dragalin, A.G.",
  title="New forms of realizability and {M}arkov's rule 
         ({R}ussian)",
  year=1980,
  journal="Doklady",
  volume=251,
  pages="534--537",
  reviews="MR 81k:03063; ZBL 481#03034",
  note="Translation {\em SM} 21, pp. 461--464"
}
		  
@article{DragalinA:tracca,
  author="Dragalin, A.G.",
  title="Transfinite Completions of Constructive Arithmetical 
			Calculus ({R}ussian)",
  year=1969,
  journal="Doklady",
  volume=189,
  pages="458--460",
  reviews="MR 41#3242; ZBL 205.310",
  note="Translation {\em SM} 10, pp. 1417--1420"
}
		  
@phdthesis{EggerzP:reamlz,
  author="Eggerz, P.",
  title="Realisierbarkeitskalk{\"u}le {\bf ML}$_0$
         und vergleichbare Theorien im Verh{\"a}ltnis zur
	Heyting-Arithmetik",
  year=1987,
  school="Ludwig-Maximilians-Universit{\"a}t, M{\"u}nchen"
}
		  
@inproceedings{ErhardT:catsc,
  author = "Th. Ehrhard",
  title = "A Categorical Semantics of Constructions",
  booktitle = "Proc. of 3rd Annual  Symposium on Logic in Computer Science",
  year = 1988,
  publisher = "IEEE Computer Soc. Press"
}
		  
@article{ErsovJ:cfft,
  author = {Yu.L. Er{\v s}ov},
  title = {Computable functionals of finite type},
  journal = {Algebra i Logika},
  volume = 11,
  number = 4,
  year = 1972
}
		  
@inproceedings{ErsovJ:modcpc,
   author =   {Yu.L. Er{\v s}ov},
   title =    {Model {{\sf C}} of Partial Continuous Functionals},
   pages =    {455-467},
   editor =    {R.O. Gandy and J.M.E. Hyland},
   booktitle = {Logic Colloquium '77},
   publisher = {North Holland Publishing Company},
   year =      1977
}
		  
@article{ErsovJ:tas,
  author = {Yu.L. Er{\v s}ov},
  title = {The Theory of {A}-spaces},
  journal = {Algebra i Logika},
  volume = 12,
  number = 4,
  year = 1972
}
		  
@article{ErsovJ:then,
   author =  {Yu.L. Er{\v s}ov},
   title =   {Theorie der {N}umerierungen},
   journal = {Zeitschrift f{\"u}r Math. Log.},
   year =    1973,
   volume =  19,
   number =  4,
   pages =   {289-388}
}
		  
@article{ErsovJ:thenII,
   author =  {Yu.L. Er{\v s}ov},
   title =   {Theorie der {N}umerierungen {II}},
   journal = {Zeitschrift f{\"u}r Math. Log.},
   year =    1975,
   volume =  21,
   number =  6,
   pages =   {473-584}
}
		  
@article{ErsovJ:thenIII,
   author =  {Yu.L. Er{\v s}ov},
   title =   {Theorie der {N}umerierungen {III}},
   journal = {Zeitschrift f{\"u}r Math. Log.},
   year =    1977,
   volume =  23,
   number =  4,
   pages =   {289-371}
}
		  
@inproceedings{FefermanS:contfc,
  author="Feferman, S.",
  title="Constructive Theories of Functions and Classes",
  year=1979,
  booktitle="Logic Colloquium '78",
  publisher={North-Holland Publishing Company},
  editor="Boffa, M. and van Dalen, D. and McAloon, K.",
  pages="159--224",
  reviews="JSL 49.308; MR 81i:03093; ZBL 441#03022"
}
		  
@inproceedings{FefermanS:lanaem,
  author="Feferman, S.",
  title="A Language and Axioms for Explicit Mathematics",
  year=1975,
  booktitle="Algebra and Logic",
  editor="Crossley, {J.N.}",
  publisher={Springer-Verlag},
  pages="87--139",
  reviews="JSL 49.308; MR 53#12899; RZH 75.11A102; ZBL 357#02029"
}
		  
@techreport{FerreiraF:extaip,
  author="Ferreira, F. and Marques, A.",
  title="Extracting Algorithms from Intuitionistic Proofs",
  institution="Universidade de Lisboa",
  number="Pr{\'e}-publica{\c{c}}{\~o}es de Matem{\'a}tica 26/96",
  year=1996
}
		  
@inproceedings{FourmanM:shelog,
  author="Fourman, M.P. and Scott, D.S.",
  title="Sheaves and Logic",
  booktitle="Applications of Sheaves",
  year=1979,
  pages="302--401",
  editor="Fourman, M.P. and Mulvey, C.J. and Scott, D.S.",
  publisher={Springer-Verlag}
}
		  
@book{FreydP:cata,
   author =    {P.J. Freyd and A. Scedrov},
   title =     {Categories, Allegories},
   year =      1991,
   publisher = {North Holland Publishing Company}
}
		  
@inproceedings{FreydP:dinff,
   author =   {P.J. Freyd and E.P. Robinson and G. Rosolini},
   title =    {Dinaturality for free},
   pages =    {107-118},
   editor =   {M.P. Fourman and P.T. Johnstone and A.M. Pitts},
   booktitle ={Proceedings of Symposium in Applications of 
		  Categories to Computer Science},
   publisher ={Cambridge University Press},
   year =     1992
}
		  
@article{FreydP:extp,
   author =  {P.J. Freyd and P. Mulry and G. Rosolini and D.S. Scott},
   title =   {Extensional {PER}s},
   journal = {Information and Computation},
   year =    1992,
   volume =  98,
   pages =   {211-227}
}
		  
@inproceedings{FreydP:polp,
   author =   {P.J. Freyd},
   title =    {P{OLYNAT} in {PER}},
   pages =    {67-68},
   editor =    {J.W. Gray and A. Scedrov},
   booktitle = {Categories in {C}omputer {S}cience and {L}ogic},
   address =   {Boulder, June 1987},
   series =    {Contemporary Mathematics},
   volume =    92,
   publisher = {American Mathematical Society},
   year =      1989
}
		  
@inproceedings{FriedmanH:appkis,
  author="Friedman, H.M.",
  title="Some Applications of {K}leene's Methods for 
	Intuitionistic Systems",
  year=1973,
  editor="Mathias, A. R. D. and Rogers, H.",
  booktitle="Cambridge Summer School in Mathematical Logic",
  publisher={Springer-Verlag},
  pages="113--170",
  reviews="MR 51#12486; RZH 74.3A36; ZBL 272#02038"
}

@article{FriedmanH:derip,
  title="On the Derivability of Instantiation Properties",
  author="Friedman, H.M.",
  journal={Journal of Symbolic Logic},
  year=1977,
  volume=42,
  pages="506--514" 
}
		  
@article{FriedmanH:dispin,
  author="Friedman, H.M.",
  title="The Disjunction Property Implies the Numerical 
			Existence Property",
  year=1975,
  journal="Proceedings of the National Academy of Sciences of
	   the United States of America",
  volume=72,
  pages="2877--2878",
  reviews="MR 52#47; ZBL 342#02012"
}
		  
@article{FriedmanH:intprw,
  title="Intuitionistically Provable Recursive Well-Orderings",
  author="Friedman, H.M. and Scedrov, A.",
  journal={Annals of Pure and Applied Logic},
  year=1986,
  volume=30,
  pages="165--171"
}

@article{FriedmanH:larsis,
  title="Large Sets in Intuitionistic Set Theory",
  author="Friedman, H.M. and Scedrov, A.",
  journal={Annals of Pure and Applied Logic},
  year=1984,
  volume=27,
  pages="1--24"
}
		  
@article{FriedmanH:setepi,
  title="Set Existence Property for Intuitionistic Theories with
			Dependent Choice",
  author="Friedman, H. M. and Scedrov, A.",
  journal={Annals of Pure and Applied Logic},
  year=1983,
  volume=25,
  pages="129--140",
  note="Corrigendum in {\em APAL} {\bf 26} (1984), p.101"
}
@article{FriedmanH:settfc,
  author="Friedman, H.M.",
  title="Set Theoretic Foundations of Constructive Analysis",
  journal="Annals of Mathematics, Series 2",
  volume=105,
  year=1977,
  pages="1--28"
}
		  
@techreport{GallierJ:proptlt,
  author="Gallier, J.",
  title="Proving Properties of Typed Lambda-Terms using
			Realizability, Covers, and Sheaves",
  year=1993,
  number="MS-CIS-93-91",
  institution="Computer and Information Science Department,
	    School of Engineering and Applied Science,
	    University of Pennsylvania, Philadelphia"
}
		  
@inproceedings{GandyR:crcfht,
  author = {R.O. Gandy and J.M.E. Hyland},
  title = {Computable and Recursively Countable Functions of Higher
		 Type},
  booktitle = {Logic Colloquium '76},
  publisher = {North-Holland},
  year = 1977
}
		  
@article{GavrilenkoJ:recrip,
  author="Gavrilenko, {\protect{Yu}}. V.",
  title="Recursive Realizability from the Intuitionistic Point 
			of View ({R}ussian)",
  year=1981,
  journal="Doklady",
  volume=256,
  pages="18--22",
  reviews="MR 82h:03067; ZBL 467#03055",
  note="Translation {\em SM} 23, pp. 9--14"
}
		  
@BOOK{Girard,
 Author = "J.-Y. Girard and Y. Lafont and P.  Taylor",
 Title = "Proofs and Types",
 Publisher = "Cambridge University Press",
 Year = 1989,
 Series = "Cambridge Tracts in Theoretical Computer Science",
 Volume = 7
}
		  
		  
@book{GirardJY:prot,
  author="Girard, J.-Y. and Lafont, Y. and Taylor, P.",
  title="Proofs and Types",
  year=1988,
  publisher="Cambridge University Press, Cambridge U.K."
}
		  
@book{GoedelK:colwII,
  author="G{\"o}del, K.",
  title="Collected Works, Volume 2",
  year=1990,
  publisher="Oxford University Press, Oxford"
}

@article{GoedelK:intaz,
  author = {K. G{\"o}del},
  title = {Zur intuitionistischen Arithmetik und Zahlentheorie},
  journal = {Ergebnisse eines mathematisches Kolloquiums},
  year = 1932,
  volume = 4,
  pages = {34-38}
}
		  
@article{GoedelK:ubeefs,
  author="G{\"o}del, K.",
  title="{\"U}ber eine bisher noch nicht ben{\"u}tzte 
         {E}rweiterung des finiten {S}tandpunktes",
  year=1958,
  journal="Dialectica",
  volume=12,
  pages="280--287",
  reviews="JSL 25.351; MR 21#1275; MR 81i:03094; ZBL 90.10"
}
		  
@article{GoodmanN:relria,
  author="Goodman, N.D.",
  title="Relativized Realizability in Intuitionistic 
	Arithmetic of all Finite Types",
  year=1978,
  journal={Journal of Symbolic Logic},
  volume=43,
  pages="23--44",
  reviews="MR 81b:03061; RZH 79.2A46; ZBL 395#03038"
}

@inproceedings{Grayson:heymis,
  author = "R.J. Grayson",
  title = "Heyting-valued Models for  Intuitionistic Set Theory",
  booktitle = "Application of Sheaves",
  editor = "M. Fourman and C. Mulvey and D.S. Scott",
  year = 1979,
  volume = 743,
  series = {Lecture Notes in Mathematics},
  pages = "402--414",
  publisher = "Springer",
  address = "Berlin"}
		  
@misc{GraysonR:appmrt,
  title="Appendix to modified realisability toposes",
  author="Grayson, R.J.",
  note="Handwritten notes from M{\"u}nster University",
  year="1982"
}
		  
@misc{GraysonR:derrmt,
  title="Derived Rules Obtained by a Model-Theoretic Approach to
			Realisability",
  author="Grayson, R.J.",
  note="Handwritten notes from M{\"u}nster University",
  year=1981,
}
		  
@misc{GraysonR:extr,
  title="Note on extensional realizability",
  author="Grayson, R.J.",
  note="Handwritten notes from M{\"u}nster University",
  year="1981"
}
		  
@misc{GraysonR:modrt,
  title="Modified realisability toposes",
  author="Grayson, R.J.",
  note="Handwritten notes from M{\"u}nster University",
  year=1981
}
		  
@misc{GraysonR:notr,
  author =	 {R. Grayson},
  title =	 {Notes on realizability},
  year =	 1982
}
		  
@article{HarnikV:lamcpt,
  author="Harnik, V. and Makkai, M.",
  title="Lambek's Categorical Proof Theory and {L}{\"a}uchli's 
		Abstract Realizability",
  year=1992,
  journal={Journal of Symbolic Logic},
  volume=57,
  pages="200--230"
}
		  
@article{HarnikV:protfi,
  author="Harnik, V.",
  title="Provably Total Functions of Intuitionistic
			Bounded Arithmetic",
  journal={Journal of Symbolic Logic},
  year=1992,
  pages="466--477",
  volume=57
}
		  
@proceedings{HeytingA:conm,
  title="Constructivity in Mathematics",
  editor="Heyting, A.",
  year=1959,
  publisher={North-Holland Publishing Company}
}

@article{HiggsD:injtch,
  author="Higgs,D.",
  title="Injectivity in the Topos of Complete Heyting Algebra valued Sets",
  journal={Canadian Journal of Mathematics},
  year=1984,
  pages="550--568",
  volume=36,
  number=3
}
		  
@book{HilbertD:grum,
  author = "D. Hilbert and P. Bernays",
  title  = "Grundlagen der Mathematik I",
  publisher = "Springer Verlag",
  Year  =  1934
}

@InProceedings{HofmannM:semaho,
  author = 	 {M.~Hofmann},
  title = 	 {Semantical Analysis of Higher-Order Abstract Syntax},
  booktitle = 	 {14th Annual Symposium on Logic in Computer Science},
  publisher =	 {IEEE Computer Society Press, Washington},
  year =	 1999,
  pages =	 {?--?}
}
@incollection{HofmannM:ssdt,
  author = "Hofmann, M.",
  title = "Syntax and Semantics of Dependent Types",
  editors = "Dybjer, P. and Pitts, A.M.",
  booktitle = "Semantic and Logic of Computation",
  publisher = "Cambridge University Press",
  year=1997
}

@incollection{HowardW:apphmf,
  author="Howard, W.A.",
  title="Appendix: Hereditarily Majorizable Functionals 
			of Finite Type",
  year=1973,
  editor="Troelstra, A. S.",
  booktitle="Metamathematical Investigation of Intuitionistic 
			Arithmetic and Analysis",
  publisher={Springer-Verlag},
  reviews="MR 48#3699; MR 56#8334; RZH 74.6A90; ZBL 275#02025",
  note="With contributions by A. S. Troelstra, 
        A. Smory{\'n}ski, J. I. Zucker and W. A. Howard",
  pages="454--461",
  reviews="MR 57#9493; RZH 74.6A114"
}
		  
@inproceedings{HowardW:fortnc,
  author = "W.A. Howard",
  title = "To {H.B. Curry}: The Formulae-as-types Notion of Construction",
  year = 1969,
  booktitle = "Essays on Combinatory Logic, Lambda Calculus, and Formalism",
  publisher = "Academic Press",
  editor = "J. Hindley and J. Seldin" 
}
		  
@inproceedings{HylandJ:algtpm,
   author =   {J.M.E. Hyland and E.P. Robinson and G. Rosolini},
   title =    {Algebraic Types in {PER} Models},
   pages =    {333-350},
   editor =    {M. Main and A. Melton and M. Mislove and D.Schmidt},
   booktitle = {Mathematical Foundations of Programming Language 
                Semantics},
   address =   {New Orleans},
   series =    {Lecture Notes in Computer Science},
   volume =    442,
   publisher = {Springer-Verlag},
   year =      1990
}
		  

@article{HylandJ:disote,
   author =  {J.M.E. Hyland and E.P. Robinson and G. Rosolini},
   title =   {The discrete objects in the effective topos},
   journal = {Proceedings of the London Mathematical Society},
   year =    1990,
   volume =  60,
   pages =   {1-60}
}
		  
@inproceedings{HylandJ:efft,
   author =   {J.M.E. Hyland},
   title =    {The effective topos},
   pages =    {165-216},
   editor =   {A.S. Troelstra and D. Van Dalen},
   booktitle ={The {L.E.J. Brouwer} Centenary Symposium},
   publisher ={North Holland Publishing Company},
   year =     1982
}
		  
@inproceedings{HylandJ:firssd,
   author =   {J.M.E. Hyland},
   title =    {First steps in Synthetic Domain Theory},
   pages =    {131-156},
   editor =    {A. Carboni and M.C. Pedicchio and G. Rosolini},
   booktitle = {Category Theory '90},
   address =   {Como},
   series =    {Lectures Notes in Mathematics},
   volume =    1144,
   publisher = {Springer-Verlag},
   year =      1992
}
		  
@article{HylandJ:fsct,
  author = {J.M.E. Hyland},
  title = {Filter Spaces and Continuous Functionals},
  journal = {Annals of Mathematical Logic},
  volume = 16,
  year = 1979
}
		  
@inproceedings{HylandJ:mrtsnp,
  author    = {J.M.E. Hyland and C.-H. L. Ong},
  title     = {Modified Realizability Toposes and Strong Normalization
	       Proofs},
  booktitle = {Typed Lambda Calculi and Applications},
  pages     = {179--194},
  editor    = {J.F. Groote and M. Bezem},
  series    = {Lecture Notes in Computer Science},
  volume    = 664,
  publisher = {Springer-Verlag},
  year      = 1993 
}
		  
@article{HylandJ:smacc,
   author =  {J.M.E. Hyland},
   title =   {A Small Complete Category},
   journal = {Journal of Pure and Applied Logic},
   year =    1988,
   volume =  40,
   pages =   {135-165}
}
		  
@article{HylandJ:trit,
   author =  {J.M.E. Hyland and P.T. Johnstone and A.M. Pitts},
   title =   {Tripos Theory},
   journal = {Math. Proc. Camb. Phil. Soc.},
   year =    1980,
   volume =  88,
   pages =   {205-232}
}
		  
@BOOK{JacobsB:cltt,
 author = "Jacobs, B.",
 title = "Categorical Logic and Type Theory",
 publisher = "Elsevier Science",
 year = 1999
}

@article{JankovV:reafpl,
  author="Jankov, V.A.",
  title="Realizable Formulas of Propositional Logic ({R}ussian)",
  journal={Doklady},
  volume=151,
  year=1963,
  pages="1035--1037",
  note="Translation {\em SM} 4, pp. 1146--1148"
}

@Book{JohnstonePT:indcta,
  editor = 	 {P.T. Johnstone and R. Par{\'e}},
  title = 	 {Indexed Categories and Their Applications},
  publisher = 	 {Sringer-Verlag, Berlin},
  year = 	 1978,
  volume = 	 661,
  series = 	 {Lecture Notes in Mathematics}
}

@article{JohnstonePT:irt,
  author = {P.T. Johnstone and E.P. Robinson},
  title = {A Note on Inequivalence of Realizability Toposes},
  journal = {Mathematical Proceedings of Cambridge Philosophical Society},
  volume = 105,
  year = 1989 }
		  
@article{JohnstonePT:locmt,
  author = 	 "P.T. Johnstone and I. Moerdijk",
  title = 	 "Local Maps of Toposes",
  journal =	 "Proc.\ London Math.\ Soc.",
  year =	 1989,
  volume =	 3,
  number =	 58,
  pages =	 "281--305"
}
		  
@Book{JohnstonePT:topt,
  author = 	 {P.T. Johnstone},
  title = 	 {Topos Theory},
  publisher = 	 {Academic Press, London},
  year = 	 1977,
  number = 	 10,
  series = 	 {LMS Mathematical Monographs}
}
		  
@book{JoyalA:algst,
   author = {Joyal, A. and Moerdijk, I.},
    title = {Algebraic Set Theory},
   series = {London Mathematical Society Lecture Note Series},
   volume = {220},
publisher = {Cambridge University Press},
  address = {Cambridge},
     year = {1995},
    pages = {viii+123}
}
		  
@article{KabakovF:derrfs,
  author="Kabakov, F.A.",
  title="On the Derivability of some Realizable Formulae
			of the Sentential Calculus ({R}ussian)",
  journal="ZMLG",
  volume=9,
  year=1963,
  pages="97--104",
  reviews="MR26#4884,ZBL112.5"
}
		  
@article{KabakovF:intdrf,
  author="Kabakov, F.A.",
  title="Intuitionistic Deducibility of some Realizable Formulae
			of Propositional Logic ({R}ussian)",
  journal={Doklady},
  year=1970,
  volume=192,
  pages="269--271",
  note="Translation {\em SM} 11, pp. 612--614",
  reviews="MR41#8209, ZBL212.312"
}
@article{KabakovF:modpba,
  author="Kabakov, F.A.",
  title="On Modelling of Pseudo-Boolean Algebras
			by Realizability ({R}ussian)",
  journal={Doklady},
  year=1970,
  volume=192,
  pages="16--18",
  note="Translation {\em SM} 11, pp. 562--564",
  reviews="MR42#43, ZBL278#02019"
}
		  
@Article{KellyGM:comlel,
  author = 	 "G.M. Kelly and F.W. Lawvere",
  title = 	 "On the Complete Lattice of Essential Localizations",
  journal =	 "Bull.\ Soc.\ Math.\ Belg.\ Ser.\ A",
  year =	 1989,
  volume =	 "XLI",
  number =	 2,
  pages =	 "289--319"
}
		  
@article{KhakhanyanV:comsct,
  author="Khakhanyan, V. {\protect{Kh}}.",
  title="Comparative Strength of Variants of {C}hurch's 
			Thesis at the Level of Set Theory ({R}ussian)",
  year=1980,
  journal={Doklady},
  volume=252,
  pages="1070--1074",
  note="Translation {\em SM}  21, pp. 894--898",
  reviews="MR 81g:03069; ZBL 482#03026"
}
		  
@article{KhakhanyanV:conicp,
  author="Khakhanyan, V. {\protect{Kh}}.",
  title="The Consistency of some Intuitionistic and 
			Constructive Principles with a Set Theory",
  year=1981,
  journal="Studia Logica",
  volume=40,
  pages="237--248",
  reviews="MR 84e:03061; ZBL 491#03019"
}
		  
@article{KhakhanyanV:conistb,
  author="Khakhanyan, V. {\protect{Kh}}.",
  title="Consistency of the Intuitionistic Set Theory with
			{B}rouwer's Principle",
  journal="Matematika",
  volume=5,
  year=1979
}
		  
@article{KhakhanyanV:conistc,
  author="Khakhanyan, V. {\protect{Kh}}.",
  title="The Consistency of Intuitionistic Set Theory with 
			{C}hurch's 
                     Principle and the Uniformization Principle ({R}ussian)",
  year=1980,
  journal="Vestnik Moskovskogo Universiteta. Seriya I. Matematika,
Mekhanika",
  volume=5,
  pages="3--7",
  reviews="MR 82b:03106; ZBL 445#03031",
  note="Translation {\em Moscow University Mathematics 
			Bulletin} 35/5, pp. 3--7"
}
		  
@article{KhakhanyanV:conistf,
  author="Khakhanyan, V. {\protect{Kh}}.",
  title="The Consistency of Intuitionistic Set Theory with Formal
                 Mathematical Analysis ({R}ussian)",
  year=1980,
  journal={Doklady},
  volume=253,
  pages="48--52",
  reviews="MR 81h:03109; ZBL 531#03036",
  note="Translation {\em SM} 22, pp. 46--50"
}
		  
@article{KhakhanyanV:nonupct,
  author="Khakhanyan, V. {\protect{Kh}}.",
  title="Nonderivability of the Uniformization Principle from
			{C}hurch's Thesis ({R}ussian)",
  journal="Matematicheskie Zametki",
  volume=43,
  year=1988,
  pages="685--691,703",
  note="Translation {\em Mathematical Notes} 43, pp. 394--398",
  review="MR89g:03089"
}

@incollection{KhakhanyanV:stct,
  author="Khakhanyan, V. {\protect{Kh}}.",
  title="Set Theory and {C}hurch's Thesis ({R}ussian)",
  year=1983,
  booktitle="Issledovaniya po Neklascheskims Logikam i Formal'nym Sistemam
		(Studies in Nonclassical logics and Formal Systems)",
  publisher="Nauka, Moskva",
  editor="Mikhajlov, A. I.",
  pages="198--208",
  reviews="MR 85d:03117"
}

@article{KipnisM:concap,
  author="Kipnis, M.M.",
  title="The Constructive Classification of Arithmetic Predicates
			and the Semantic Bases of Arithmetic ({R}ussian)",
  year=1968,
  journal="Zapiski",
  volume=8,
  pages="53--65",
  note="Translation {\em Seminars in Mathematics. V.A.Steklov
			Mathematical Institute Leningrad}  8(1970), pp. 22--27. 
			This volume appeared as: A.O. Slisenko
			(ed.), {\em Studies in Constructive Mathematics and
			Mathematical Logic. Part II}. Consultants Bureau, 
			New York, London"
}
		  
@article{KipnisM:reapf,
  author="Kipnis, M.M.",
  title="On the Realizations of Predicate Formulas ({R}ussian)
			({E}nglish summary)",
  journal={Zapiski},
  year=1971,
  volume=20,
  pages="40--48",
  note="Translation  {\em Journal of Soviet Mathematics} 
		1(1973), pp. 22--27",
  reviews="ZBL 222#02021"
}
		  
@inproceedings{KleeneSC:claeim,
  author="Kleene, S.C.",
  title="Classical Extensions of Intuitionistic Mathematics",
  year=1965,
  booktitle="LMPS 2",
  editor="Bar-Hillel, Y.",
  publisher={North-Holland Publishing Company},
  pages="31--44",
  reviews="JSL 40.508; MR 35#28  ; ZBL 192.30"
}
		  
@inproceedings{KleeneSC:conffi,
  author="Kleene, S.C.",
  title="Constructive Functions in ``{T}he {F}oundations 
			of {I}ntuitionistic {M}athematics''",
  year=1968,
  booktitle="LMPS 3",
  editor="van Rootselaar, B. and Staal, J. F.",
  publisher={North-Holland Publishing Company},
  pages="137--144",
  reviews="MR 40#5424; ZBL 191.287"
}
		  
@inproceedings{KleeneSC:couf,
   author =   {S.C. Kleene},
   title =    {Countable Functionals},
   pages =    {81-100},
   editor =    {A. Heyting},
   booktitle = {Constructivity in Mathematics},
   publisher = {North Holland Publishing Company},
   year =      1959
}

@article{KleeneSC:diseie,
  author="Kleene, S.C.",
  title="Disjunction and Existence under Implication in 
			Elementary Intuitionistic Formalisms",
  year=1962,
  journal={Journal of Symbolic Logic},
  volume=27,
  pages="11--18",
  note="Addenda in {\em JSL} {\bf 28} (1963), pp. 154--156",
  reviews="JSL 28.166; JSL 29.146; MR 27#1368; MR 32#5515;
          ZBL 112.245"
}
		  
@article{KleeneSC:ffqftII,
  author = {S.C. Kleene},
  title = {Recursive Functionals and Quantifiers of Finite Types {II}},
  journal = {Trans.\ Amer.\ Math.\ Soc},
  volume = 108,
  year = 1963
}
		  
@book{KleeneSC:forrff,
  author="Kleene, S.C.",
  title="Formalized Recursive Functionals and Formalized Relizability",
  year=1969,
  series="Memoirs of the American Mathematical Society",
  publisher={American Mathematical Society},
  volume="89",
 reviews="MR 39#5319; ZBL 184.20"
}
		  
@book{KleeneSC:fouim,
  author="Kleene, S.C. and Vesley, R.E.",
  title="The Foundations of Intuitionistic Mathematics, 
			especially in relation to recursive functions",
  year=1965,
  publisher={North-Holland Publishing Company},
  reviews="JSL 31.258; MR 31#1190; ZBL 133.246",
}
		  
@article{KleeneSC:intint,
  author="Kleene, S.C.",
  title="On the Interpretation of Intuitionistic Number Theory",
  year=1945,
  journal={Journal of Symbolic Logic},
  volume=10,
  pages="109--124",
  reviews="JSL 12.91 ; MR 7.406"
}
		  
@book{KleeneSC:intmm,
  author="Kleene, S.C.",
  title="Introduction to metamathematics",
  year=1952,
  publisher={North-Holland Publishing Company},
  reviews="JSL 19.215; JSL 25.280; JSL 33.290; JSL 35.350; 
  JSL38.333; MR 14.525 ; ZBL 47.7",
  note="Co-publisher: Wolters--Noordhoff; 8th revised ed.1980." 
}
		  
@article{KleeneSC:logcr,
  author="Kleene, S.C.",
  title="Logical Calculus and Realizability",
  year=1965,
  journal="Acta Philosophica Fennica",
  volume=18,
  pages="71--80",
  reviews="MR 33#5485; ZBL 133.252"
}
		  
@inproceedings{KleeneSC:rea,
  author="Kleene, S. C.",
  title="Realizability",
  year=1957,
  booktitle="Summaries of Talks presented at the Summer
		Institute for Symbolic Logic",
  publisher="Institute for Defense Analyses, Communications
			Research Division, Princeton",
  pages="100--104",
  reviews="JSL 27.242; MR 21#2590; RZH 62.11A63; ZBL 88.249",
  note="Also in {\em \cite{HeytingA:conm}}, pp. 285--289. 
	Errata in {\em \cite{KleeneSC:fouim}}, page 192"
}
@inproceedings{KleeneSC:rears,
   author =   {S.C. Kleene},
   title =    {Realizability: a Retrospective Survey},
   pages =    {95-112},
   editor =    {A.R.D. Mathias and H. Rogers},
   booktitle = {Cambridge Summer School in Mathematical Logic},
   series =    {Lecture Notes in Mathematics},
   volume =    337,
   publisher = {Springer-Verlag},
   year =      1973
}

@article{KleeneSC:reasac,
  author="Kleene, S.C.",
  title="Realizability and {S}hanin's Algorithm for the 
			Constructive Deciphering of Mathematical Sentences",
  year=1960,
  journal="Logique et Analyse, Nouvelle S{\'e}rie",
  volume=3,
  pages="154--165",
  reviews="JSL 27.243"
}
		  
@article{KleeneSC:rfqftI,
  author = {S.C. Kleene},
  title = {Recursive Functionals and Quantifiers of Finite Types {I}},
  journal = {Trans.\ Amer.\ Math.\ Soc},
  volume = 91,
  year = 1959
}
		  
@inproceedings{KleeneSC:rfqftrI,
  author = {S.C. Kleene},
  title = {Recursive Functionals and Quantifiers of Finite Types 
                    Revisited {I}},
  booktitle = {Generalized Recursion Theory {II}},
  editor = {J.E. Fenstad and R.O. Gandy and G.E. Sacks},
  pages = {185--222},
  year = 1978
}
		  
@article{KobayashiS:reaigi,
  author="Kobayashi, S. and Tatsuta, M.",
  title="Realizability Interpretation of Generalized Inductive
			Definitions",
  year=1994,
  journal="Theoretical Computer Science",
  volume=131,
  pages="121--138"
}
		  
@article{KohlenbachU:poihma,
  author="Kohlenbach, U.W.",
  title="Pointwise Hereditary Majorization and some Applications",
  year=1992,
  journal="Archive for Mathematical Logic",
  pages="227--241",
  volume=31
}
		  
@phdthesis{KohlenbachU:thesis,
  author="Kohlenbach, U.W.",
  title="Theorie der majorisierbaren und stetigen {F}unktionale und
		ihre {A}nwendung bei der {E}xtraktion von {S}chranken 
		aus inkonstruktiven {B}eweisen:
		effektive {E}indeutigkeitsmodule bei besten 
		{A}pproximationen aus ineffektiven
		{E}indeutigkeitsbeweisen",
  year=1990,
  school="J.W. Goethe-Universit{\"a}t, Frankfurt am Main"
}
		  
@article{KreiselG:forsia,
  author="Kreisel, G. and Troelstra, A.S.",
  title="Formal Systems for some Branches of Intuitionistic 
			Analysis",
  year=1970,
  journal={Annals of Pure and Applied Logic},
  volume=1,
  pages="229--387",
  note="Addendum in {\em APAL} 3, pp. 437--439",
  reviews="MR 41#8210; MR 45#1729; ZBL 211.11; ZBL 231#02041"
}
		  
@inproceedings{KreiselG:fouil,
  author="Kreisel, G.",
  title="Foundations of Intuitionistic Logic",
  year=1962,
  booktitle="LMPS",
  editor="Nagel, E. and Suppes, P. and Tarski, A.",
  publisher="Stanford University Press, Stanford",
  pages="198--210",
  reviews="JSL 30.243; MR 27#3529; ZBL 133.248"
}
		  
@incollection{KreiselG:iafft,
  author = {G. Kreisel},
  title = {Interpretation of Analysis by means of Functionals of
		 Finite Type},
  booktitle = {Constructivity in Mathematics},
  pages = {101--128},
  editor = {A. Heyting},
  publisher = {North-Holland},
  year = 1959,
  reviews="JSL 36.169; MR 21#5568; ZBL 134.10"		  
}
		  
@article{KreiselG:varhtf,
  author="Kreisel, G.",
  title="A Variant to {H}ilbert's Theory of the Foundations
			of Arithmetic",
  journal="British Journal for the Philosophy of Science",
  year=1953,
  volume=4,
  pages="107--127"
}
		  
@article{KreiselG:weacipl,
  author="Kreisel, G.",
  title="On Weak Completeness of Intuitionistic Predicate Logic",
  year=1962,
  journal={Journal of Symbolic Logic},
  volume=27,
  pages="139--158",
  reviews="JSL 34.119; MR 28#5000; ZBL 117.10"
}
		  
@article{KrolM:disepi,
  author="Krol', M.D.",
  title="Disjunctive and Existential Properties of
	    Intuitionistic Analysis with {K}ripke's scheme ({R}ussian)",
  journal={Doklady},
  volume=234,
  year=1977,
  note="Translation {\em SM} 18, pp. 755--758"
}
		  
@article{KrolM:varfcp,
  author="Krol', M.D.",
  title="Various Forms of the Continuity Principle ({R}ussian)",
  year=1983,
  journal={Doklady},
  volume=271,
  pages="33--36",
  note ="Translation {\em SM}  28, pp. 27--30",
  reviews="MR 84m:03094; ZBL 549#03052"
}
		  
@inproceedings{KrolM:verr,
  author="Krol', M.D.",
  title="On a Version of Realizability ({R}ussian)",
  year=1992,
  booktitle="XI Interrepublican Conference on Mathematical
   Logic, University of Kazan, October 6--8, 1992",
  pages=81
}

		  
@techreport{KurtzS:confsc,
  author="Kurtz, S.A. and Mitchell, J.C. and O'Donnell, M.J.",
  title="Connecting Formal Semantics to Constructive Intuitions",
  institution="Department of Computer Science, University of
		Chicago",
  year=1992,
  number="CS 92--01"
}
		  
@InProceedings{LambekJ:indpft,
  author = 	 {J. Lambek and P.J. Scott},
  title = 	 {Independence of Premisses and the Free Topos},
  booktitle = 	 {Proc. Symp. Constructive Math},
  volume =	 873,
  series =	 {Lecture Notes in Mathematics},
  year =	 1981,
  pages =	 {191--207}
}

@book{LambekJ:inthoc,
  author="Lambek, J. and Scott, P. J.",
  title="Introduction to Higher Order Categorical Logic",
  publisher="Cambridge University Press, Cambridge",
  year=1986
}
		  
@Article{LambekJ:intttf,
  author = 	 {J. Lambek and P.J. Scott},
  title = 	 {Intuitionistic Type Theory and the Free Topos},
  journal = 	 {Journal of Pure and Applied Algebra},
  year = 	 1980,
  volume =	 19,
  pages =	 {215--257}
}
		  
@Article{LambekJ:proip,
  author = 	 {J. Lambek and P.J. Scott},
  title = 	 {New Proofs of some Intutitionistic Principles},
  journal = 	 {Zeitschrift f{\"u}r Math. Log.},
  year = 	 1983,
  volume =	 29,
  pages =	 {493--504}
}
		  
@inproceedings{LauchliH:absnri,
  author="L{\"a}uchli, H.",
  title="An Abstract Notion of Realizability for which 
			Intuitionistic Predicate Calculus is Complete",
  year=1970,
  booktitle="Intuitionism and Proof Theory",
  editor="Kino, A. and Myhill, J.R. and Vesley, R.E.",
  publisher = {North-Holland},
  pages="227--234",
  reviews="MR 42#5778; ZBL 216.5"
}
		  
@article{LawvereFW:adjf,
 author={F.W.~Lawvere},
 title={Adjointness in Foundations},
 journal={Dialectica},
 volume=23,
 year=1969,
 pages={281--296}
}

@incollection {LawvereFW:daccc,
   author = {F. W. Lawvere},
    title = {Diagonal arguments and cartesian closed categories},
booktitle = {Category Theory, Homology Theory and their Applications, II
             (Battelle Institute Conference, Seattle, Wash., 1968, Vol.
             Two)},
    pages = {134--145},
publisher = {Springer-Verlag},
  address = {Berlin},
     year = 1969
}


@inproceedings{LawvereFW:equhcs,
 author={F.W.~Lawvere},
 title={Equality in Hyperdoctrines and the Comprehension Schema as an
Adjoint Functor},
 booktitle={Applications of Categorical Algebra},
 editor={A.~Heller},
 publisher={American Mathematical Society, Providence RI},
 year=1970,
 pages={1--14}
}

@InProceedings{LawvereFW:somtfc,
  author = 	 {F.W. Lawvere},
  title = 	 {Some Thoughts on the Future of Category theory},
  booktitle = 	 {Category Theory. Proceedings of the International Conference held in Como, Italy, July 22--28, 1990},
  editor =	 {A. Carboni and M.C. Pedicchio and G. Rosolini},
  volume =	 1488,
  series =	 {Lecture Notes in Mathematics},
  year =	 1991,
  publisher =	 {Springer-Verlag},
  pages =	 {1--13}
}

@Unpublished{LawvereFW:topgco,
  author = 	 "F.W. Lawvere",
  title = 	 "Toposes Generated by Codiscrete Objects in Combinatorial
		  Topology and Functional Analysis",
  note = 	 "Notes for Colloquium lectures given at North Ryde, New
		  South Wales, Australia on April 18, 1989 and at Madison,
		  USA, on December 1, 1989",
  year = 	 1989
}
		  
@InCollection{LeivantD:conpp,
  author = 	 {D. Leivant},
  title = 	 {Contracting Proofs to Programs},
  booktitle = 	 {Logic and Computer Science},
  pages =	 {279--327},
  publisher =	 {Academic Press, London},
  year =	 1990,
  editor =	 {P.~Odifreddi}
}
		  
@InCollection{LeivantD:pealcf,
  author = 	 {D. Leivant},
  title = 	 {Peano's Lambda Calculus: The functional abstraction implicit
                  in arithmetic},
  booktitle = 	 {Church Memorial Volume: Logic, Language, and Computation},
  publisher =	 {Kluwer Academic Publishing},
  year = 	 2000,
  editor =	 {C.A. Anderson and M. Zeleny},
  note =	 {To Appear}
}
		  
@Article{LeivantD:pealcf:abstract,
  author = 	 {D. Leivant},
  title = 	 {Peano's Lambda Calculus: The functional abstraction implicit
                  in arithmetic},
  journal = 	 {Bulletin of Symbolic Logic},
  year = 	 1998,
  volume =	 4,
  pages =	 {451--452}
}
		  
@Article{LeivantD:ramrcc,
  author = 	 {D. Leivant},
  title = 	 {Ramified recurrence and computational complexity {III}:
                  Higher type recurrence and elementary complexity},
  journal = 	 {Annals of Pure and Applied Logic},
  year = 	 1999,
  volume =	 96,
  number =	 3,
  pages =	 {209--229}
}
		  
@InProceedings{LeivantD:reafpc,
  author = 	 {D. Leivant},
  title = 	 {Reasoning about functional programs and complexity classes 
                  associated with type disciplines}, 
  booktitle = 	 {Proceedings of the Twenty Fourth Annual Symposium on the
                  Foundations of Computer Science},
  pages =	 {460--469},
  year =	 1983,
  publisher =	 {IEEE Computer Society, Washington}
}

@incollection{LifschitzV:calnn,
  author="Lifschitz, V.",
  title="Calculable Natural Numbers",
  year=1985,
  booktitle="Intensional Mathematics",
  editor="Shapiro, S.",
  publisher={North-Holland},
  pages="173--190",
  reviews="MR 86m:03093; ZBL 606#03017"
}
		  
@article{LifschitzV:conaec,
  author="Lifschitz, V.",
  title="Constructive Assertions in an Extension of 
			Classical Mathematics",
  year=1982,
  journal={Journal of Symbolic Logic},
  volume=47,
  pages="359--387",
  reviews="MR 84a:03075; ZBL 488#03034"
}
		  
@article{LifschitzV:ct0,
  author="Lifschitz, V.",
  title="{CT$_0$ is stronger than CT$_0$!}",
  year=1979,
  journal="Proceedings of the American Mathematical Society",
  volume=73,
  pages="101--106",
  reviews="MR 80b:03094; RZH 79.9A42; ZBL 379#02012"
}
		  
@inproceedings{LiptonJ:conksr,
  author="Lipton, J.",
  title="Constructive {K}ripke Semantics and Realizability",
  booktitle="Logic from Computer Science",
  editor="Moschovakis, Y.N.",
  year=1990,
  publisher={Springer},
  note="Also as a Technical Report, from Cornell University, nr.90--71"
}	
		  
@article{LiptonJ:intrsc,
  author="Lipton, J. and {O'Donnell}, M.J.",
  title="Some Intuitions behind Realizability Semantics for
			Constructive Logic: Tableaux and {L}{\"a}uchli 
			Countermodels",
  journal={Annals of Pure and Applied Logic},
  year=1996,
  volume=81,
  pages="187--239"
}
		  
@PhdThesis{LongleyJ:reatls,
  author = 	 {J. Longley},
  title = 	 {Realizability Toposes and Language Semantics},
  school = 	 {Edinburgh University},
  year = 	 1995
}
		  
@techreport{LongleyJ:seqrf,
  author = {J. Longley},
  title = {The Sequentially Realizable Functionals},
  institution = {University of Edinburgh},
  number = {ECS--LFCS--98--402},
  year = 1998 
}
		  
@article{LongleyJ:uadtrm,
  author = {J.R. Longley and A.K. Simpson},
  title = {A Uniform Approach to Domain Theory in Realizability
		 Models},
  journal = {Mathematical Structures in Computer Science},
  volume = 7,
  pages = {469--505},
  year = 1997 
}
		  
@inproceedings{LongoG:ccceets,
  author = {G. Longo and E. Moggi},
  title = {Cartesian Closed Categories of Enumerations for Effective
		 Type Structures},
  booktitle = {Semantics of Data Types},
  editor = {G. Kahn and D. MacQueen and G. Plopkin},
  volume = 173,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  year = 1984
}
		  
@article{LongoG:connda,
   author =  {G. Longo and E. Moggi},
   title =   {Constructive Natural Deduction and its $\omega$-set 
              Interpretation},
   journal = {Mathematical Structures in Computer Science},
   year =    1991,
   volume =  1,
   pages =   {215-254}
}
		  
@article{LongoG:herpef,
   author =  {G. Longo and E. Moggi},
   title =   {The Hereditary Partial Effective Functionals and Recurion
		  Theory in Higher Type},
   journal = {Journal of Symbolic Logic},
   year =    1984,
   volume =  49,
   pages =   {127-140}
}
		  
@article{LongoG:sembq,
  author = "G. Longo and L. Cardelli",
  title = "A Semantic Basis for Quest",
  journal = "Journal of Functional Programming",
  year = 1991,
  volume = 1,
  number = 4,
  pages = "417--458"
}
		  
@BOOK{LuoOxford ,
 Author = "Z. Luo",
 Title = "Computation and Reasoning -- A Type Theory for Computer Science",
 Publisher = "Oxford University Press",
 Volume =  11,
 Series = "Monographs on Computer Science",
 Year = 1994
}
		  
@phdthesis{LuoZ:extcoc,
  author = "Z. Luo",
  title = "An Extended Calculus of Constructions",
  year = 1990,
  school = "University of Edinburgh",
  note = "Available as report ECS-LFCS-90-118"
}

@article{LuoZ:prosdr,
  author = "Z. Luo",
  title = "Program Specification and Data Refinement in Type Theory",
  journal = "Mathematial Structures in Computer Science",
  year = "1993",
  volume = 3
}
		  
@Article{MakkaiM:fibfip,
  author = 	 {M. Makkai},
  title = 	 {The Fibrational Formulation of Intuitionistic
                  Predicate Logic. {I}: Completeness According to
                  {G}{\"o}del, {Kripke}, and {L}{\"a}uchli},
  journal = 	 {Notre Dame Journal of Formal Logic},
  year = 	 1993,
  volume = 	 34,
  pages = 	 {334--377}
}
		  
@Book{MakkaiM:firocl,
  author = 	 {M.~Makkai and G.E.~Reyes},
  title = 	 {First Order Categorical Logic},
  publisher = 	 {Springer-Verlag, Berlin},
  year = 	 1977,
  volume = 	 611,
  series = 	 {Lecture Notes in Mathematics}
}
		  
@article{MaksimovaL:impfam,
  author="Maksimova, L.L. and Shekhtman, V.B. and Skvortsov, D.P.",
  title="The Impossibility of a Finite Axiomatization of
			{M}edvedev's Logic of Finitary Problems ({R}ussian)",
  journal={Doklady},
  volume=245,
  year=1979,
  pages="1051--1054",
  note="Translation  {\em SM} 20, pp. 394--398",
  reviews="MR80e:03021, ZBL 439#03008"
}
		  
@inproceedings{MartinLofP:conmcp,
  author="Martin--{L\"of}, P.",
  title="Constructive Mathematics and Computer Programming",
  year=1982,
  booktitle="LMPS 6",
  editor="Cohen, L.J. and Los, J. and Pfeiffer, H. and Podewski, K.-P.",
  publisher={North-Holland},
  pages="153--175",
  reviews="MR 85d:03112; MR 86c:03051; ZBL 443#68039; ZBL 552#03040"
}
		  
@book{MartinLofP:inttt,
  author="Martin--{L\"of}, P.",
  title="Intuitionistic Type Theory. 
         Notes by Giovanni Sambin of a series of 
         lectures given in Padua, June 1980",
  year=1984,
  publisher={Bibliopolis, Napoli},
  pages="xii+92pp",
  reviews="JSL 51.1075; MR 86j:03005; ZBL 571#03030"
}
		  
@inproceedings{MartinLofP:ittpp,
  author = "Martin-L{\"o}f, P.",
  title = "An intuitionisitc theory of types, Predicative part",
  editors = "Rose, E.H. and Sheperdson J.C.",
  pages =  "73--118",
  booktitle = "Logic Colloquium 1973",
  poublisher = "North-Holland",
  year = "1975"
}
		  
@inproceedings{McCartyD:infscr,
  author="McCarty, D.C.",
  title="Information Systems, Continuity and Realizability",
  year=1984,
  booktitle="Logics of Programs",
  editor="Clarke, E. and Kozen, D.",
  publisher={Springer},
  series="Lecture Notes in Computer Science",
  volume=164,
  pages="341--359",
  reviews="ZBL 558#03031"
}
		  
@incollection{McCartyD:iscr,
  author = {D.C. McCarty},
  title = {Information Systems, Continuity and Realizability},
  booktitle = {Logics of Programs},
  series = {Lecture Notes in Computer Science},
  volume = 164,
  editor = {E. Clarke and D. Cozen},
  publisher = {Springer-Verlag},
  year = 1984
}
		  
@article{McCartyD:marpid,
  author="McCarty, D.C.",
  title="Markov's Principle, isols and {D}edekind Finite Sets",
  journal={Journal of Symbolic Logic},
  year=1988,
  volume=53,
  pages="1042--1069"
}
		  
@article{McCartyD:pola,
  author="McCarty, D.C.",
  title="Polymorphism and Apartness",
  journal="The Notre Dame Journal of Formal Logic",
  volume=32,
  year=1991,
  pages="513--532"
}
		  
@phdthesis{McCartyD:reaarm,
   author =  {D.C. McCarty},
   title =   {Realizability and Recursive Mathematics},
   year =    1984,
   school =  {University of Oxford},
   type =    {D.{P}hil. {T}hesis}
}
		  
@techreport{McCartyD:rearm,
  author="McCarty, D.C.",
  title="Realizability and Recursive Mathematics",
  institution="Department of Computer Science, Carnegie-Mellon University",
  year=1984,
  number="CMU--CS--84--131",
  note="Report version of the author's PhD thesis, Oxford University 1983"
}
		  
@article{McCartyD:subcr,
  author="McCarty, D.C.",
  title="Subcountability under Realizability",
  journal="The Notre Dame Journal of Formal Logic",
  volume=27,
  year=1986,
  pages="210--220",
  reviews="MR87h:03108"
}


@Book{McLartyC:elecet,
  author = 	 {C. {McL}arty},
  title = 	 {Elementary Categories, Elementary Toposes},
  publisher = 	 {Clarendon Press},
  year = 	 {1995}
}
		  
@article{MedvedevY:finp,
  author="Medvedev, {\protect{Yu}}.T.",
  title="Finite Problems ({R}ussian)",
  year=1962,
  journal={Doklady},
  volume=142,
  pages="1015--1018",
  note="Translation {\em SM} 3, pp. 227--230",
  reviews="JSL 38.330; MR 24#A3067; ZBL 286#02028"
}
		  
@inproceedings{MedvedevY:intint,
  author="Medvedev, {\protect{Yu}}.T.",
  title="An Interpretation of Intuitionistic Number Theory",
  year=1973,
  booktitle="LMPS 4",
  editor="Suppes, P. and Moisil, G.C. and Joja, A.",
  publisher={North-Holland},
  pages="129--136",
  reviews="MR 56#5240"
}
		  
@article{MedvedevY:intlff,
  author="Medvedev, {\protect{Yu}}.T.",
  title="Interpretation of Logical Formulae by means of Finite Problems 
		  and its Relation to the Realizability Theory ({R}ussian)",
  year=1963,
  journal={Doklady},
  volume=148,
  pages="771--774",
  note="Translation  {\em SM} 4, pp. 180--183",
  reviews="JSL 38.330; MR 26#4904; ZBL 218#02048"
}
		  
@article{MedvedevY:intlff66,
  author="Medvedev, {\protect{Yu}}.T.",
  title="Interpretation of Logical Formulae by means of 
			Finite Problems ({R}ussian)",
  year=1966,
  journal={Doklady},
  volume=169,
  pages="20--23",
  note="Translation {\em SM} 7, pp. 857--860",
  reviews="JSL 38.330; MR 38#37; ZBL 192.38"
}
		  
@article{MedvedevY:locfap,
  author="Medvedev, {\protect{Yu}}.T.",
  title="Locally Finitary Algorithmic Problems ({R}ussian)",
  year=1972,
  journal={Doklady},		  
  volume=203,
  pages="285--288",
  note="Errata {\em Ibidem} 204, pp. 1286. 
	Translation {\em SM} 13, pp. 382--386",
  reviews="MR 47#24; RZH 72.8A90; ZBL 262#02034"
}
		  
@article{MedvedevY:metpua,
  author="Medvedev, {\protect{Yu}}.T.",
  title="A Method for Proving the Unsolvability of 
			Algorithmic Problems ({R}ussian)",
  year=1969,
  journal={Doklady},
  volume=185,
  pages="1232--1235",
  note="Translation {\em SM} 10, pp. 495--498",
  reviews="MR 40#4112; ZBL 193.316"
}
		  
@BOOK{MilnerR:defsml,
  author = "R.~Milner and M.~Tofte and R.~Harper",
  title = "The Definition of Standard ML",
  publisher = "MIT Press",
  year = 1990
}

@article{MintsG:compr,
  author="Mints, G.E.",
  title="The Completeness of Provable Realizability",
  journal="The Notre Dame Journal of Formal Logic",
  year=1989,
  volume=30,
  pages="420--441"
}
		  
@BOOK{MitchellJC:fpl,
 author = "Mitchell, J.C.",
 title = "Foundations of Programming Languages",
 publisher = "MIT Press",
 year = 1996
}
		  
@article{MoggiE:pmceo,
  author = {E. Moggi},
  title = {Partial Morphisms in Categories of Effective Objects},
  journal = {Information and Computation},
  volume = 76,
  year = 1988
}
		  

@article{MoschovakisJ:clavic,
  author="Moschovakis, J.R.",
  title="A Classical View of the Intuitionistic Continuum",
  year=1996,
  journal={Annals of Pure and Applied Logic},
  volume=81,
  pages="9--24"
}
		  
@inproceedings{MoschovakisJ:disdtc,
  author="Moschovakis, J.R.",
  title="A Disjunctive Decomposition Theorem for Classical Theories",
  booktitle="Constructive Mathematics",
  year=1981,
  editor="Richman, F.",
  publisher={Springer},
  pages="250--259"
}
		  
@inproceedings{MoschovakisJ:disefi,
  title="Disjunction and Existence in Formalized Intuitionistic Analysis",
  author="Moschovakis, J.R.",
  booktitle="Sets, Models, and Recursion Theory",
  editor="Crossley, J.N.",
  publisher={North-Holland},
  year=1967,
  pages="309--331"
}
		  
@inproceedings{MoschovakisJ:inttlc,
  author="Moschovakis, J.R.",
  title="An Intuitionistic Theory of Lawlike, Choice and Lawless Sequences",
  booktitle="Logic Colloquium '90",
  publisher={Springer},
  pages="191--209",
  year=1993,
  note="(Lecture Notes in Logic 2)"
}
		  
@inproceedings{MoschovakisJ:klerdn,
  author="Moschovakis, J.R.",
  title="{K}leene's Realizability and ``Divides'' 
			Notions for Formalized Intuitionistic Mathematics",
  year=1980,
  booktitle="The Kleene Symposium",
  editor="Barwise, K.J. and Keisler, H.J. and Kunen, K.",
  publisher={North-Holland},
  pages="167--179",
  reviews="MR 81m:03071; ZBL 517#03025"
}
@article{MoschovakisJ:nonrf,
  author="Moschovakis, J.R.",
  title="Can there be no nonrecursive functions?",
  year=1971,
  journal={Journal of Symbolic Logic},
  volume=36,
  pages="309--315",
  reviews="MR 45#3162; RZH 72.3A42; ZBL 247#02036"
}
		  
@article{MoschovakisJ:rells,
  author="Moschovakis, J.R.",
  title="More about Relatively Lawless Sequences",
  year=1994,
  journal={Journal of Symbolic Logic},
  volume=59,
  pages="813--829"
} 


@article{MoschovakisJ:topisi,
  author="Moschovakis, J.R.",
  title="A Topological Interpretation of Second-order
			Intuitionistic Arithmetic",
  journal="Compositio Mathematica",
  volume=26,
  year=1973,
  pages="261--275"
}
		  
@article{MulryP:genbft,
   author =  {P. Mulry},
   title =   {Generalized {B}anach-{M}azur Functionals 
		  in the Topos of Recursive Sets},
   journal = {Journal of Pure and Applied Algebra},
   year =    1982,
   volume =  26,
   pages =   {71-83}
}
		  
		  
@article{MyhillJ:const,
  author="Myhill, J.R.",
  title="Constructive Set Theory",
  year=1975,
  journal={Journal of Symbolic Logic},
  volume=40,
  pages="347--382",
  reviews="JSL 46.868; MR 52#2830; RZH 77.1A40; ZBL 314#02045"
}

@article{MyhillJ:indf,
  title="A note on Indicator-Functions",
  author="Myhill, J.R.",
  journal="Proceedings of the American Mathematical Society",
  year=1973,
  volume=29,
  pages="181--183" 
}

	  
@inproceedings{MyhillJ:proizf,
  author="Myhill, J.R.",
  title="Some Properties of Intuitionistic {Z}ermelo-{F}raenkel
			Set Theory",
  year=1973,
  editor="Mathias, A.R.D. and Rogers, H.",
  booktitle="Cambridge Summer School in Mathematical Logic",
  publisher={Springer},
  pages="206--231"
}
		  
@article{NelsonD:recfin,
  author="Nelson, D.",
  title="Recursive Functions and Intuitionistic Number Theory",
  year=1947,
  journal="Transactions of the American Mathematical Society",
  volume=61,
  pages="307--368,556",
  reviews="JSL 12.93 ; MR 10.3; ZBL 58.249"
}


@book{NordstromB:promlt,
  author = "B. Nordstr{\"o}m and K. Petersson and J.M. Smith",
  title = "Programming in Martin L{\"o}f's Type Theory",
  publisher = "Oxford University Press",
  volume =  7,
  series = "Monographs on Computer Science",
  year = 1990
}
		  
@techreport{OostenJ:axices,
  author = {J. van Oosten and A.K. Simpson},
  title = {Axioms and (Counter)examples in Synthetic Domain Theory},
  year = 1998,
  number = {1080},
  institution = {Department of Mathematics, Utrecht University}
}
		  
@article{OostenJ:axihok,
  author="J. van Oosten",
  title="Axiomatizing higher-order {K}leene realizability",
  year=1994,
  journal={Annals of Pure and Applied Logic},
  pages="87--111",
  volume=70
}
		  
@inproceedings{OostenJ:casfft,
  author="van Oosten, J.",
  title="A Combinatory Algebra for Sequential Functionals of Finite
		 Type",
  year=1999,
  booktitle="Models and Computability",
  editor="Cooper, S.B. and Truss, J.K.",
  publisher={Cambridge University Press},
  pages="389--406",
}
		  
@techreport{OostenJ:casfft:tr,
  author = {J. van Oosten},
  title = {A Combinatory Algebra for Sequential Functionals of Finite
		 Type},
  institution = {University of Utrecht},
  number = 996,
  year = 1997 
}
		  
@phdthesis{OostenJ:exer,
  title="Exercises in Realizability",
  author="J. van Oosten",
  school="Universiteit van Amsterdam",
  year=1991
}
		  
@article{OostenJ:extlrh,
  author="J. van Oosten",
  title="Extension of {L}ifschitz' Realizability to Higher Order
		Arithmetic, and a Solution to a Problem of {F}. {R}ichman",
  journal={Journal of Symbolic Logic},
  year=1991,
  volume=56,
  pages="964--973"
}
		  
@Article{OostenJ:extrea,
  author = 	 "J. van Oosten",
  title = 	 "Extensional Realizability",
  journal =	 "Annals of Pure and Applied Logic",
  year =	 1997,
  volume =	 "84",
  pages =	 "317--349"
}

@article{OostenJ:lifr,
  author="J. van Oosten",
  title="Lifschitz' realizability",
  journal={Journal of Symbolic Logic},
  year=1990,
  volume=55,
  pages="805--821"
}

@article{OostenJ:mrt,
  author = {J. van Oosten},
  title = {The Modified Realizability Topos},
  journal = {Journal of Pure and Applied Algebra},
  volume = 116,
  pages = {273--289},
  year = 1997
}

@article{OostenJ:remlrt,
  author="J. van Oosten",
  title="Two Remarks on the {L}ifschitz Realizability Topos",
  year=1996,
  volume=61,
  journal={Journal of Symbolic Logic},
  pages="70-79"
}
		  
@article{OostenJ:sempdj,
  author="J. van Oosten",
  title="A Semantical Proof of {D}e {J}ongh's Theorem",
  year=1991,
  pages="105--114",
  journal="Archive for Mathematical Logic"
}
		  
@article{PhoaW:bdgm,
  author = {W.K.-S. Phoa},
  title = {Building Domains from Graph Models},
  journal = {Mathematical Structures in Computer Science},
  volume = 2,
  year = 1992 
}
		  
@PhdThesis{PhoaW:domtrt,
  author = 	 {W. Phoa},
  title = 	 {Domain Theory in Realizability Toposes},
  school = 	 {Cambridge University},
  year = 	 1990
}
		  
@inproceedings{PhoaW:effdis,
   author =   {W. Phoa},
   title =    {Effective Domains and Intrinsic Structure},
   pages =    {366-377},
   editor =    {J. Mitchell},
   booktitle = {Proceedings of the 5th Annual IEEE Symposium on Logic in
		  Computer Science}, 
   address =   {Philadelphia, Pennsylvania},
   publisher = {IEEE Computer Society Press},
   year =      1990
}
		  
@techreport{PhoaW:fttetms,
  author = {W.K.-S. Phoa},
  title = {An Introduction to Fibrations, Topos Theory, the Effective Topos
           and Modest Sets},
  number = {ECS-LFCS-92-208},
  institution = {Department of Computer Science, University of Edinburgh},
  year = 1992 }
		  
@article{PhoaW:rcet,
  author = {W.K.-S. Phoa},
  title = {Relative Computability in the Effective Topos},
  journal = {Math.\ Proc.\ Camb.\ Phil.\ Soc},
  volume = 106,
  year = 1989 
 }

		 
@article{PhoaW:relcet,
  author="Phoa, W.",
  title="Relative Computability in the Effective Topos",
  journal="Mathematical Proceedings of the Cambridge
			Philosophical Society",
  year=1989,
  pages="419--420",
  volume=106
}

@inproceedings{PhoaW:tmd,
  author = {W.K.-S. Phoa},
  title = {From Term Models to Domains},
  booktitle = {Proceedings of Theoretical Aspects of Computer Software,
		 Sendai},
  publisher = {Springer LNCS 526},
  year = 1991 
}
		  
@techreport{PittsAM:catl,
  author =	 {A.M.~Pitts},
  title =	 {Categorical Logic},
  institution =	 {University of Cambridge Computer Laboratory},
  year =	 1995,
  type =	 {Technical Report},
  number =	 367,
  note =         {To appear as a chapter of \emph{Handbook of Logic in 
                  Computer Science, Vol.~V} (Oxford University Press).} 
}
		  
@article{PittsAM:concfo,
  author =	 {A.M.~Pitts},
  title =	 {Conceptual Completeness for First Order
                  Intuitionistic Logic: an Application of Categorical
                  Logic},
  journal =	 {Annals Pure Applied Logic},
  volume =	 41,
  year =	 1989,
  pages =	 {33--81},
}
		  
@article{PittsAM:intsoq,
  author =	 {A.M.~Pitts},
  title =	 {On an Interpretation of Second Order Quantification
                  in First Order Intuitionistic Propositional Logic},
  journal =	 {Jour.\ Symbolic Logic},
  volume =	 57,
  year =	 1992,
  pages =	 {33--52}
}
		  
@phdthesis{PittsAM:thet,
  author =	 {A.M.~Pitts},
  title =	 {The Theory of Triposes},
  school =	 {Cambridge University},
  year =	 1981,
}
		  
@article{PliskoV:absrpf,
  author="Plisko, V.E.",
  title="Absolute Realizability of Predicate Formulas  ({R}ussian)",
  year=1983,
  journal="Izv. Akad. Nauk.",
  volume=47,
  pages="315--334",
  note="Translation {\em Math. Izv.} 22, pp. 291--308",
  reviews="MR 85f:03063; ZBL 554#03029"
}
		  
@article{PliskoV:conrur,
  author="Plisko, V.E.",
  title="On the Concept of Relatively Uniform Realizability of
			Propositional Formulas ({R}ussian)",
  journal="Vestnik Moskovskogo Universiteta Seriya I.
			Mathematika, Mekhanika",
  year=1992,
  pages="77--79",
  note="Translated in {\it Moscow University Mathematics
			Bulletin} 47 (1992), 41--42"
}
		  
@incollection{PliskoV:forsr,
  author="Plisko, V.E.",
  title="A Certain Formal System that is connected with 
			Realizability ({R}ussian)",
  year=1974,
  booktitle="Teoriya Algorifmov i Matematicheskaya Logika: Sbornik Statej
	(Theory of Algorithms and Mathematical Logic. Collection 
	of articles dedicated to Andrej Andrejevich Markov)",
  editor="Kushner, B.A. and Nagornyi, N.M.",
  publisher="Vychislitel'nyj Tsentr Akademii Nauk SSSR",
  pages="148--158,215",
  reviews="MR 53#10561; RZH 74.10A128; ZBL 298#02024"
}
		  
@inproceedings{PliskoV:intpfc,
  author="Plisko, V.E.",
  title="On Interpretations of Predicate Formulae that are 
			connected with Constructive Logic ({R}ussian)",
  year=1974,
  booktitle="3 Vsesoyuznaya Konferentsiya po Matematicheskoj Logike.
		Tezitsy Doklady i Soobshcheniya (3rd All-Union Conference on
		Mathematical Logic)",
  pages="170--172"
}
		  
@article{PliskoV:noncrp,
  author="Plisko, V.E.",
  title="The Nonarithmeticity of the Class of Realizable 
			Predicate Formulas ({R}ussian)",
  year=1977,
  journal="Izv. Akad. Nauk.",
  volume=41,
  pages="483--502",
  note="Translation {\em Math. Izv.} 11, pp. 453--471",
  reviews="MR 57#16031; RZH 77.10A24; ZBL 373#02032"
}
		  
@article{PliskoV:reapf,
  author="Plisko, V.E.",
  title="On Realizable Predicate Formulae ({R}ussian)",
  year=1973,
  journal={Doklady},
  volume=212,
  pages="553--556",
  note="Translation {\em SM} 14, pp. 1420--1424",
  reviews="MR 48#10779; RZH 74.1A104; ZBL 295#02009"
}
		  
@article{PliskoV:recrcp,
  author="Plisko, V.E.",
  title="Recursive Realizability and Constructive Predicate 
			Logic ({R}ussian)",
  year=1974,
  journal={Doklady},
  volume=214,
  pages="520--523",
  note="Translation {\em SM} 15, pp. 193--197",
  reviews="MR 54#2433; RZH 74.6A141; BL 299#02027"
}
		  
@article{PliskoV:varnrp,
  author="Plisko, V.E.",
  title="Some Variants of the Notion of Realizability 
			for Predicate Formulas ({R}ussian)",
  year=1976,
  journal={Doklady},
  volume=226,
  pages="61--64",
  note="Translation {\em SM} 17, pp. 59--63",
  reviews="MR 58#172 ; RZH 76.6A47; ZBL 358#02035"
}
		  
@article{PliskoV:varnrp78,
  author="Plisko, V.E.",
  title="Some Variants of the Notion of Realizability for 
			Predicate Formulas ({R}ussian)",
  year=1978,
  journal="Izv. Akad. Nauk.",
  volume=42,
  pages="637--653",
  note="Translation {\em Math. Izv.} 12, pp. 588--604",
  reviews="MR 80b:03035; RZH 78.10A41; ZBL 384#03042"
}
		  
@book{PourEl:comap,
  author = 	 "M.B.~Pour-El and J.I.~Richards",
  title = 	 "Computability in Analysis and Physics",
  publisher = 	 "Springer-Verlag",
  year = 	 1989
}
		  
@incollection {ProiettiM:conbpm,
   author = {Proietti, M.},
    title = {Connections between Partial Maps Categories and Tripos Theory},
booktitle = {Category Theory and Computer Science (Edinburgh, 1987)},
    pages = {254--269},
   series = {Lecture Notes in Computer Science},
   volume = {283},
publisher = {Springer-Verlag},
  address = {Berlin},
     year = {1987}
}
		  
@article{RenardelG:extbia,
  author="Renardel de Lavalette, G.R.",
  title="Extended Bar Induction in Applicative Theories",
  year=1990,
  journal={Annals of Pure and Applied Logic},
  volume=50,
  pages="139--189"
}
		  
@phdthesis{RenardelG:thetae,
  author="Renardel de Lavalette, G.R.",
  title="Theories with Type-free Application and Extended Bar Induction",
  year=1984,
  school="Universiteit van Amsterdam"
}
		  
@article{ReusB:estt,
  author = "B. Reus",
  title = "Extensional {$\Sigma$}-Spaces in Type Theory",
  journal = "Applied Categorical Structures",
  note = "To Appear",
  year = 1999
}
		  
@article{ReusB:gensdt,
  author =	 {B. Reus and T. Streicher},
  title =	 {General Synthetic Domain Theory---A Logical
                  Approach},
  year =	 1999,
  volume =	 9,
  pages =	 {177--223},
  journal =	 {Mathematical Structures in Computer Science}
}
		  
@PhdThesis{ReusB:provsd,
  author = 	 {B. Reus},
  title = 	 {Program Verification in Synthetic Domain Theory},
  school = 	 {L{\"u}dwig-Maximilians-Universit{\"a}t M{\"u}nchen},
  year = 	 1995,
  type = 	 {Dokt.{D}iss.},
  note = 	 {Shaker Verlag, Aachen}
}
		  
@inproceedings{ReusB:syndtt,
  author = "B. Reus",
  title = "Synthetic Domain Theory in Type Theory: Another Logic of
		  Computable  Functions", 
  year = 1996,
  booktitle = "Theorem Proving in Higher Order Logics:
               9th International Conference, {TPHOL}s'96",
  publisher = "Springer",
  volume = "1125",
  series = {Lecture Notes in Computer Science},
  editor = "von~Wright, J. and Grundy, J. and Harrison, J." ,
  pages = "363--381"
}
		  
@article{RobinsonE:colcet,
   author =  {E.P. Robinson and G. Rosolini},
   title =   {Colimit Completions and the Effective Topos},
   journal = {Journal of Symbolic Logic},
   year =    1990,
   volume =  55,
   pages =   {678-699}
}

@inproceedings{RobinsonE:comp,
   author =   {E.P. Robinson},
   title =    {How Complete is {PER}?},
   pages =    {106-111},
   editor =    {A.R. Meyer},
   booktitle = {Proceedings of the 4th Annual IEEE Symposium on Logic in
		  Computer Science}, 
   address =   {Asilomar},
   publisher = {IEEE Computer Society Press},
   year =      1989
}

@article{RobinsonT:intkmp,
  author="Robinson, T.T.",
  title="Interpretations of {K}leene's Metamathematical Predicate 
			{$\Gamma\mid A$} in Intuitionistic Arithmetic",
  year=1965,
  journal={Journal of Symbolic Logic},
  volume=30,
  pages="140--154",
  reviews="MR 33#7254; ZBL 133.249",
}
		  
@article{RoseG:procr,
  author="Rose, G.F.",
  title="Propositional Calculus and Realizibility",
  year=1953,
  journal="Transactions of the American Mathematical Society",
  volume=75,
  pages="1--19",
  reviews="JSL 19.126; MR 15.1; ZBL 53.199"
}
		  
@unpublished{RosickyJ:carcec,
  author = 	 {J. Rosick{\'y}},
  title = 	 {Cartesian Closed Exact Completions},
  note = 	 {Available from the Hypatia Electronic Library: 
		  {{\tt http://hypatia.dcs.qmw.ac.uk}}},
  year =	 {1997}
}

@article{RosoliniG:aboms,
  author="Rosolini, G.",
  title="About Modest Sets",
  journal="International Journal of Foundations of Computer Science",
  year=1990,
  volume=1,
  pages="341--353"
}
		  
@inproceedings{RosoliniG:catec,
   author =   {G. Rosolini},
   title =    {Categories and Effective Computations},
   pages =    {1-11},
   editor =    {D.H. Pitt and A. Poign{\'e} and D.E. Rydeheard},
   booktitle = {{C}ategory {T}heory and {C}omputer {S}cience},
   address =   {Edinburgh},
   series =    {Lectures Notes in Computer Science},
   volume =    283,
   publisher = {Springer-Verlag},
   year =      1987
}
		  
@PhdThesis{RosoliniG:cet,
  author = 	 {G. Rosolini},
  title = 	 {Continuity and Effectiveness in Topoi},
  school = 	 {University of Oxford},
  year = 	 1986,
}
		  
@INPROCEEDINGS{RosoliniG:expmq,
  author = "G. Rosolini",
  title = "An {ExPer} Model for {Q}uest",
  booktitle = "MFPS'91",
  editor = "S. Brookes and M. Main and A. Melton and M. Mislove and
            D. Schmidt",
  year = 1991,
  publisher = "Springer",
  volume = 598,
  series = {Lecture Notes in Computer Science},
  pages = "436--445"
}
		  
@article{ScarpelliniB:modia,
  author="Scarpellini, B.",
  title="A Model for Intuitionistic Analysis",
  year=1970,
  journal="Commentarii Mathematici Helvetici",
  volume=45,
  pages="440--471",
  reviews="MR 43#7300; ZBL 213.12"
}
		  
@article{ScarpelliniB:newrni,
  author="Scarpellini, B.",
  title="A New Realizability Notion for Intuitionistic Analysis",
  journal={ZLGM},
  volume=23,
  year=1977,
  pages="137--167"
}
		  
@article{ScedrovA:difeca,
  author="Scedrov, A.",
  title="Differential Equations in Constructive Analysis and in
			the Recursive Realizability Topos",
  journal="Journal of Pure and Applied Algebra",
  year=1984,
  volume=33,
  pages="69--80"
}
		  
@inproceedings{ScedrovA:frisfc,
  author="Scedrov, A. and Scott, P. J.",
  title="A note on the {F}riedman slash and {F}reyd covers",
  year=1982,
  booktitle="The L.E.J. Brouwer Centenary Symposium",
  editor="Troelstra, A.S. and van~Dalen, D.",
  publisher={North-Holland},
  pages="443--452",
  reviews="MR 85d:03118; ZBL 529#03039"
}
		  
@article{ScedrovA:impeub,
  title="On the Impossibility of Explicit Upper Bounds on Lengths
		of some Provably Finite Algorithms in Computable Analysis",
  author="Scedrov, A.",
  journal={Annals of Pure and Applied Logic},
  year=1986,
  volume=32,
  pages="291--297"
}
		  
@inproceedings{ScedrovA:recrsc,
  author="Scedrov, A.",
  title="Recursive Realizability Semantics for {C}alculus of
			{C}onstructions. {P}reliminary Report",
  year=1990,
  booktitle="Logical Foundations of Functional Programming",
  editor="Huet, G.",
  publisher="Addison-Wesley Publishing Company",
  pages="419--430"
}
		  
@article{ScedrovA:weamp,
  author="Scedrov, A. and R.E. Vesley",
  title="On a Weakening of {M}arkov's Principle",
  year=1983,
  volume=23,
  pages="153--160",
  journal="Archiv"
}
		  
@misc{ScottD:chutau,
   author =    {D.S. Scott},
   title =     {Church's Thesis and a Unification of Types},
   booktitle = {Lecture at the Conference on Church's Thesis: Fifty Years 
                Later},
   year =      1986,
   address =   {Utrecht June}
}
		  
@article{ScottD:dattl,
   author =  {D.S. Scott},
   title =   {Data Types as Lattices},
   journal = {SIAM Journal of Computing},
   year =    1976,
   volume =  5,
   number =  3,
   pages =   {522-587}
}
		  
@article{ScottD:exttii,
  author="Scott, D.S.",
  title="Extending the Topological Interpretation to
			Intuitionistic Analysis",
  journal="Compositio Mathematica",
  year=1968,
  volume=20,
  pages="194--210"
}
		  
@unpublished{ScottD:newcds,
  author = 	 {D.S. Scott},
  title = 	 {A new category? {D}omains, Spaces and Equivalence
		  Relations}, 
  note = 	 {Manuscript},
  year =	 {1996}
}
		  
@inproceedings{ScottD:reltc,
   author =   {D.S. Scott},
   title =    {Relating Theories of the $\lambda$-calculus},
   pages =    {403-450},
   editor =    {R. Hindley and J. Seldin},
   booktitle = {To {H.B. Curry}: Essays in Combinatory Logic, Lambda
		  Calculus and Formalisms},
   publisher = {Academic Press},
   year =      1980
}
		  
@Unpublished{ScottDS:logtcc,
  author = 	 "D.S. Scott and S. Awodey and A. Bauer and L. Birkedal and
		  J. Hughes",  
  title = 	 "{L}ogics of {T}ypes and {C}omputation at {C}arnegie
		  {M}ellon {U}niversity", 
  note = 	 "\newline\texttt{http://www.cs.cmu.edu/Groups/LTC/}"
}
		  
@inproceedings{ScowcroftP:disnep,
  author="Scowcroft, P.",
  title="The Disjunction and Numerical Existence Properties for
			Intuitionistic Analysis",
  booktitle="Logical Methods",
  editor="Crossley, J.N. and Remmel, J.B. and Shore, R.A. and
			Sweedler, M.E.",
  year=1993,
  publisher="Birkha{\"u}ser Boston, Inc., Boston MA",
  pages="747--781"
}
		  
@article{ShaninN:algkdm,
  author="Shanin, N.A.",
  title="{\"U}ber einen {A}lgorithmus zur konstruktiven 
			{D}echiffrierung mathematischer {U}rteile 
			({R}ussian) ({G}erman summary)",
  year=1958,
  journal="ZLGM",
  volume=4,
  pages="293--303",
  reviews="MR 21#5566; ZBL 92.11"
}
		  
@article{ShaninN:coniaf,
  author="Shanin, N.A.",
  title="Concerning the Constructive Interpretation of 
			Auxiliary Formulas {I} ({R}ussian)",
  year=1964,
  journal="Trudy Ordena Lenina Matematicheskogo Instituta imeni
		V. A. Steklova. Akademiya Nauk SSSR",
  volume=72,
  pages="348--379",
  note="Translation {\em AMS Transl.} 99, pp. 233--275",
  reviews="MR 36#1324; ZBL 249#02013"
}
		  
@article{ShaninN:conimj,
  author="Shanin, N.A.",
  title="On the Constructive Interpretation of Mathematical 
			Judgements ({R}ussian)",
  year=1958,
  journal="Trudy Ordena Lenina Matematicheskogo Instituta imeni
		V. A. Steklova. Akademiya Nauk SSSR",
  volume=52,
  pages={226--311},
  note="Translation {\em AMS Transl.} 23, pp. 108--189",
  reviews="JSL 31.258; MR 21#2; ZBL 92.254"
}
		  
@inproceedings{SmithJ:intkst,
  author="Smith, J.M.",
  year=1993,
  title="An Interpretation of {K}leene's Slash in Type Theory",
  booktitle="Logical Environments",
  editor="Huet, G. and Plotkin, G.",
  publiher="Cambridge University Press, Cambridge (U.K.)",
  pages="189--197"
}
		  
@inproceedings{StaplesJ:comrcf,
  author="Staples, J.",
  title="Combinator Realizability of Constructive Finite 
			Type Analysis",
  year=1973,
  editor="Mathias, A.R.D. and Rogers, H.",
  booktitle="Cambridge Summer School in Mathematical Logic",
  publisher={Springer},
  pages="253--273",
  reviews="MR 50#63; RZH 74.3A39; ZBL 272#02037"
}
		  
@article{StaplesJ:comrcm,
  author="Staples, J.",
  title="Combinator Realizability of 
			Constructive {M}orse Theory",
  year=1974,
  journal={Journal of Symbolic Logic},
  volume=39,
  pages="226--234",
  reviews="MR 51#74; RZH 75.8A81; ZBL 306#02023"
}
		  
@article{SteinM:gentet,
  author="Stein, M.",
  title="A General Theorem on Existence Theorems",
  year=1981,
  journal="ZLGM",
  volume=27,
  pages="435--452",
  reviews="JSL 52.561; MR 83e:03089; ZBL 473#03050"
}
		  

@article{SteinM:inthaa,
  author="Stein, M.",
  title="Interpretations of {H}eyting's Arithmetic -- 
			{A}n Analysis by means of a Language with Set Symbols",
  year=1980,
  journal={AML},
  volume=19,
  pages="1--31",
  reviews="MR 82i:03067; ZBL 453#03062"
}
@article{SteinM:inthae,
  author="Stein, M.",
  title="Interpretationen der {H}eyting--{A}rithmetik endlicher 
			{T}ypen",
  year=1979,
  journal="Archiv",
  volume=19,
  pages="175--189",
  reviews="MR 81i:03092; RZH 80.1A35; ZBL 411#03051"
}

@techreport{StrahmT:parate,
  author="Strahm, T.",
  title="Partial Applicative Theories and Explicit
			Substitutions",
  institution="{Institut f\"ur Informatik und angewandte
			Mathematik, Universit\"at Bern}",
  number="IAM 93--008",
  year=1993
}
		  
@article{StreicherT:dirdt,
  author = "T. Streicher",
  title = "Dependence and independece results for (impredicative) calculi of
           dependent types", 
  journal = "Mathematical Structures in Computer Science",
  year = 1992,
  volume = 2,
  pages = "29--54"
}

%%%%%%%%%%%%%%%%%%%%%%%		  
		  
@article{StreicherT:indipa,
  author = "T. Streicher",
  title = "Independence of the Induction Principle and the Axiom of Choice in the Pure Calculus of Constructions",
  journal = "Theoretical Computer Science",
  year = 1992,
  volume = 103,
  pages = "395--408"
}
		  
@booklet{StreicherT:invitt,
  author = "T. Streicher",
  title = "Investigations Into Intensional Type Theory",
  year = 1994,
  howpublished = "Habilitationsschrift, Universit{\"a}t M{\"u}nchen"
}
		  
@techreport{StreicherT:matipc,
  author="Streicher, T.",
  title="Mathematical Independencies in the Pure Calculus of
	Constructions",
  institution="Fakult{\"a}t f{\"u}r {M}athematik und {I}nformatik,
	{U}niversit{\"a}t {P}assau",
  year=1991,
  number="MIP--909"
}
		  
@book{StreicherT:semttc,
  author = "T. Streicher",
  title = "Semantics of Type Theory, Correctness, Completeness and
		  Independence Results", 
  publisher = "Birkh{\"a}user",
  year = 1991
}
		  
@article{SwaenM:chamlm,
  author="Swaen, M.D.G.",
  title="{A Characterization of ${\bf ML}$ in Many-Sorted
			Arithmetic with Conditional Application}",
  journal={Journal of Symbolic Logic},
  year=1992,
  volume=57,
  pages="924--953"
}
		  
@article{SwaenM:logfoi,
  author="Swaen, M.D.G.",
  title="The Logic of First-Order Intuitionistic Type Theory with
		Weak Sigma-Elimination",
  journal={Journal of Symbolic Logic},
  year=1991,
  volume=56,
  pages="467--483"
}


@phdthesis{SwaenM:weasse,
  author="Swaen, M.D.G.",
  title="Weak and Strong Sum-Elimination in Intuitionistic Type Theory",
  school="Universiteit van Amsterdam",
  year=1989
}

@incollection{TaitW:reaits,
  author="Tait, W.W.",
  title="A Realizability Interpretation of the 
			Theory of Species",
  year=1975,
  booktitle="Logic Colloquium",
  editor="Parikh, R.J.",
  publisher={Springer},
  pages="240--251",
  reviews="MR 52#5380; RZH 75.12A42; ZBL 328#02014"
}

@inproceedings{TaitW:reaitt,
   author =    {W.W. Tait},
   booktitle = {Logic Colloquium},
   title =     {A Realizability Interpretation of the Theory of Species},
   year =      1975,
   volume =    453,
   pages =     {240-251},
   publisher = {Springer-Verlag},
   series =    {Lectures Notes in Mathematics},
   editor =    {R. Parikh},
   address =   {Boston}
}

@inproceedings{TatsutaM:monrdp,
  author="Tatsuta, M.",
  title="Monotone Recursive Definition of Predicates and its
			Realizability Interpretation",
  year=1991,
  booktitle="Proceedings of Theoretical Aspects of Computer
	Software",
  publisher={Springer},
  pages="38--52"
}

@article{TatsutaM:prosur,
  author="Tatsuta, M.",
  title="Program Synthesis using Realizability",
  journal="Theoretical Computer Science",
  year=1991,
  volume=90,
  pages="309--353",
}


@inproceedings{TatsutaM:reaicd,
  author="Tatsuta, M.",
  title="Realizability Interpretation of Coinductive Definitions
			and Program Synthesis with Streams",
  booktitle="Proceedings of International Conference on Fifth
	Generation Computer Systems",
  year=1992,
  pages="666--673"
}

@inproceedings{TaylorP:fixppsd,
  author = "P. Taylor",
  title = "The Fixed Point Property in Synthetic Domain Theory",
  booktitle = "6th Symp. on {L}ogic in {C}omputer {S}cience",
  year = 1991,
  pages = "152--160",
  publisher = "IEEE Computer Society Press"
}

@article{TharpL:quaist,
  author="Tharp, L.H.",
  title="A Quasi--Intuitionistic Set Theory",
  year=1971,
  journal={Journal of Symbolic Logic},
  volume=36,
  pages="456--460",
  reviews="MR 45#6617; RZH 72.6A59; ZBL 247#02055"
}

@article{TompkinsR:klerri,
  author="Tompkins, R.R.",
  title="On {K}leene's Recursive Realizability as an 
		Interpretation for Intuitionistic Elementary Number Theory",
  year=1968,
  journal="Notre Dame Journal of Formal Logic",
  volume=9,
  pages="289--293",
  reviews="JSL 35.475; MR 39#3975; ZBL 179.11"
}


@inproceedings{TroelstraA:axiimi,
  author="Troelstra, A.S.",
  title="Axioms for Intuitionistic Mathematics Incompatible 
			with Classical Logic",
  year=1977,
  booktitle="LMPS 5",
  editor="Butts, R.E. and Hintikka, J.",
  publisher="D. Reidel, Dordrecht and Boston",
  volume=1,
  pages="59--84",
  reviews="MR 57#12185; ZBL 375#02010"
}

@techreport{TroelstraA:comtnr,
  author="Troelstra, A.S.",
  title="Computability of Terms and Notions of Realizability for
                     Intuitionistic Analysis",
  year=1971,
  institution="Department of Mathematics, University of	Amsterdam",
  number="71--02"
}


@inproceedings{TroelstraA:comtrc,
  author="Troelstra, A.S.",
  title="Comparing the Theory of Representations and Constructive
			Mathematics",
  booktitle="Computer Science Logic. 5th workshop, CSL '91",
  editor="B{\"o}rger, E. and J{\"a}ger, G. and
		{Kleine B\"uning}, H. and Richter, M.M.",
  publisher={Springer},
  year=1992,
  pages="382--395",
}


@book{TroelstraA:conm,
  author="Troelstra, A.S. and van Dalen, D.",
  title="Constructivism in Mathematics",
  publisher={North-Holland},
  year=1988,
  note="2 volumes"
}
		  
@inproceedings{TroelstraA:extbit,
  author="Troelstra, A.S.",
  title="Extended Bar Induction of Type Zero",
  year=1980,
  booktitle="The Kleene Symposium",
  editor="Barwise, K.J. and Keisler, H.J. and Kunen, K.",
  publisher={North-Holland},
  pages="277--316",
  reviews="MR 82f:03054; ZBL 444#03031"
}


@inproceedings{TroelstraA:intsoa,
  author="Troelstra, A.S.",
  title="Notes on Intuitionistic Second Order Arithmetic",
  year=1973,
  editor="Mathias, A.R.D. and Rogers, H.",
  booktitle="Cambridge Summer School in Mathematical Logic",
  publisher={Springer},
  pages="171--205",
  reviews="MR 51#81; RZH 74.3A38; ZBL 275#02036"
}


@proceedings{TroelstraA:metiia,
  editor="Troelstra, A.S.",
  title="Metamathematical Investigation of Intuitionistic 
			Arithmetic and Analysis",
  year=1973,
  publisher={Springer},
  reviews="MR 48#3699; MR 56#8334; RZH 74.6A90; ZBL 275#02025",
  note="With contributions by A.S. Troelstra, 
			C.A. Smory{\'n}ski, J.I. Zucker and W.A. Howard"
}


@article{TroelstraA:modift,
  author="Troelstra, A.S.",
  title="Some Models for Intuitionistic Finite Type Arithmetic
			with Fan Functional",
  year=1977,
  journal={Journal of Symbolic Logic},
  pages="194--202",
  volume=42
}


@article{TroelstraA:noneoc,
  author="Troelstra, A.S.",
  title="A note on non--extensional operations in 
	connection with continuity and recursiveness",
  year=1977,
  journal="Indagationes Mathematicae",
  volume=39,
  pages="455--462",
  reviews="MR 57#12186; RZH 78.7A62; ZBL 368#02026"
}

@techreport{HiggsD:catabs},
  author="Higgs,D.",
  title="A Category Approach to Boolean-valued Set Theory",
  year=1973,
  institution="University of Waterloo"
}

@inproceedings{TroelstraA:notria,
  author="Troelstra, A.S.",
  title="Notions of Realizability for Intuitionistic Arithmetic and 
		  Intuitionistic Arithmetic in all Finite Types",
  year=1971,
  booktitle="The Second Scandinavian Logic Symposium",
  editor="Fenstad, J.E.",
  publisher={North-Holland},
  pages="369--405",
  reviews="JSL 40.625; MR 49#23; RZH 72.1A72; ZBL 227#02015"
}


@inproceedings{TroelstraA:rea,
  author="Troelstra, A.S.",
  title="Realizability",
  year=1998,
  booktitle="Handbook of Proof Theory",
  editor="Buss, S.R.",
  publisher={North-Holland},
  pages="407--473",
 }

@article{TsejtinG:disrfc,
  author="Tsejtin, G. S.",
  title="The Disjunctive Rank of the Formulas of Constructive
			Arithmetic ({R}ussian)",
  year=1968,
  journal={Zapiski},
  volume=8,
  pages="260--271",
  note="Translation {\em Seminars in Mathematics. V.A.Steklov
			Mathematical Institute Leningrad} 8(1970), 
			pp. 126--132.  This volume appeared as: A.O. Slisenko
			(ed.), {\em Studies in Constructive Mathematics and
			Mathematical Logic. Part II}. Consultants Bureau, 
			New York, London"
}


@book{VanDalenD:conm,
   author =    {D. van Dalen and A.S. Troelstra},
   title =     {Constructivism in Mathematics},
   year =      1988,
   publisher = {North Holland Publishing Company}
}

@article{VarpahovskijF:clarpf,
  author="Varpahovskij, F.L.",
  title="A Class of Realizable Propositional Formulas",
  year=1971,
  journal={Zapiski},
  volume=1,
  pages="8--23",
  note="Translation {\em  Journal of Soviet Mathematics}
			 {\bf 1},1--11 (1973)"
}

@inproceedings{VesleyR:palsks,
  author="Vesley, R.E.",
  title="A Palatable Substitute for {K}ripke's Schema",
  booktitle="Intuitionism and Proof Theory",
  editor="Kino, A. and Myhill, J.R. and Vesley, R.E.",
  year=1970,
  publisher={North-Holland},
  pages="197--207"
}

@article{VesleyR:reabs,
  author="Vesley, R.E.",
  title="Realizing {B}rouwer's sequences",
  journal={Annals of Pure and Applied Logic},
  volume=81,
  year=1996,
  pages="25--74"
}

@inproceedings{VoronkovA:compss,
  author="Voronkov, A.",
  title="On Completeness of Program Synthesis Systems",
  booktitle="Computer Science Logic. 5th workshop, CSL '91",
  editor="B{\"o}rger, E. and J{\"a}ger, G. and
	{Kleine B\"uning}, H. and Richter, M.M.",
  publisher={Springer},
  year=1992,
  pages="411--418"
}

@techreport{VoronkovA:nreacs,
  author="Voronkov, A.",
  title="N-realizability: one more constructive semantics",
  year=1991,
  institution="Department of Mathematics, Monash University,
			Australia",
  number="71"
}

@misc{WehmeierK:fraha,
  author="Wehmeier, K.F.",
  title="Fragments of {HA} based on {$\Sigma_1$}-induction",
  year=1996,
  note="Preprint. Part of the author's dissertation project
	at the University of M{\"u}nster, Westphalia, Germany"
}