@InProceedings{martinlof1971hauptsatz,
  Title     = {Hauptsatz for the intuitionistic theory of iterated
                  inductive definitions},
  Author    = {Martin-L{\"o}f, Per},
  Booktitle = {Proceedings of the 2nd Scandinavian logic symposium},
  Year      = 1971,
  Editor    = {Fenstad, Jan Erik},
  Publisher = {North-Holland},
	Series    = {Studies in Logic and the Foundations of Mathematics},
	Volume    = {63},
  Pages     = {179 -- 216},
}

@incollection{Martin-Lof-1972,
	Author = {Martin-L{\"o}f, Per},
	Booktitle = {Twenty-five years of constructive type theory ({V}enice, 1995)},
	Mrclass = {03B15 (03F55)},
	Mrnumber = 1686864,
	Pages = {127--172},
	Publisher = {Oxford University Press},
        Editor = {Giovanni Sambin and Jan M. Smith},
	Series = {Oxford Logic Guides},
	Title = {An intuitionistic theory of types},
	Volume = 36,
	Year = 1998}

@incollection{Martin-Lof-1973,
	Author = {Martin-L{\"o}f, Per},
	Booktitle = {Logic Colloquium '73, Proceedings of the Logic Colloquium},
	Editor = {H.E. Rose and J.C. Shepherdson},
	Mrclass = {02C15 (02D99)},
	Mrnumber = {0387009 (52 \#7856)},
	Mrreviewer = {Horst Luckhardt},
	Pages = {73--118},
	Publisher = {North-Holland},
	Series = {Studies in Logic and the Foundations of Mathematics},
	Title = {An intuitionistic theory of types: predicative part},
	Volume = 80,
	Year = 1975}


@TechReport{hml75,
  author = 	 {Hancock, Peter and Martin-L\"{o}f, Per},
  title = 	 {Syntax and semantics of the language of primitive
                  recursive functions},
  institution =  {University of Stockholm},
  year = 	 1975,
  number = 	 3,
  address = 	 {Stockholm, Sweden}
}

@incollection{Martin-Lof-1979,
	Author = {Martin-L{\"o}f, Per},
	Booktitle = {Logic, Methodology and Philosophy of Science VI, Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover 1979},
        Editor = {L. Jonathan Cohen and Jerzy {Łoś} and Helmut Pfeiffer and Klaus-Peter Podewski},
	Doi = {10.1016/S0049-237X(09)70189-2},
	Mrclass = {03F50 (03B70 03F55 68Q45)},
	Mrnumber = {682410 (85d:03112)},
	Mrreviewer = {B. H. Mayoh},
	Pages = {153--175},
	Publisher = {North-Holland},
	Series = {Studies in Logic and the Foundations of Mathematics},
	Title = {Constructive mathematics and computer programming},
	Url = {http://dx.doi.org/10.1016/S0049-237X(09)70189-2},
	Volume = 104,
	Year = 1982}

@book{martin-lof:bibliopolis,
	Author = {Martin-L{\"o}f, Per},
	Isbn = {88-7088-105-9},
	Mrclass = {03B15 (03F50 03F55)},
	Mrnumber = {769301 (86j:03005)},
	Mrreviewer = {M. M. Richter},
	Pages = {iv+91},
	Publisher = {Bibliopolis},
	Series = {Studies in Proof Theory},
	Subtitle = {Notes by Giovanni Sambin},
	Title = {Intuitionistic type theory},
	Volume = {1},
	Year = {1984}}


@article{martin2006100,
	Author = {Martin-L{\"o}f, Per},
	Journal = {The Computer Journal},
	Number = {3},
	Pages = {345--350},
	Publisher = {BCS},
	Title = {100 years of {Z}ermelo's axiom of choice: what was the problem with it?},
	Volume = {49},
	Year = {2006}}