schwichtenberg.bib

% This file was created with JabRef 2.7b.
% Encoding: ISO8859_1

@ARTICLE{abbottAltenkirchGhani2005containers,
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
  title = {Containers: Constructing strictly positive types},
  journal = {Theoretical Computer Science},
  year = {2005},
  volume = {342},
  pages = {3 -- 27},
  number = {1},
  file = {:abbottAltenkirchGhani2005containers.pdf:PDF},
  issn = {0304-3975},
  keywords = {Type theory},
  owner = {csfnf},
  timestamp = {2011.02.15}
}

@ARTICLE{aczel1999typesandsets,
  author = {Peter Aczel},
  title = {On Relating Type Theories and Set Theories},
  journal = {Lecture Notes In Computer Science},
  year = {1999},
  volume = {1657},
  pages = {1--18},
  file = {:aczel1999typesandsets.pdf:PDF},
  owner = {csfnf},
  publisher = {Springer-Verlag London, UK},
  timestamp = {2010.01.13}
}

@INCOLLECTION{aczel1977indDef,
  author = {Peter Aczel},
  title = {An Introduction to Inductive Definitions},
  booktitle = {Handbook of Mathematical Logic},
  publisher = {Elsevier},
  year = {1977},
  pages = {739--782},
  owner = {csfnf},
  timestamp = {2010.05.29}
}

@INPROCEEDINGS{altenkirchMorris2009indexedCont,
  author = {Altenkirch, T. and Morris, P.},
  title = {Indexed Containers},
  booktitle = {Logic In Computer Science},
  year = {2009},
  pages = {277 -285},
  file = {:altenkirchMorris2009indexedCont.pdf:PDF},
  issn = {1043-6871},
  keywords = {Agda system;core type theory;data type-generic programming;data type-generic
	reasoning;indexed containers;inductive families;polymorphic functions;functional
	programming;genetic algorithms;},
  owner = {csfnf},
  timestamp = {2011.02.04}
}

@INPROCEEDINGS{nordvallforsbergAltenkirchMorrisSetzer2011catsemindind,
  author = {Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik
	and Setzer, Anton},
  title = {A categorical semantics for inductive-inductive definitions},
  booktitle = {Conference on Algebra and Coalgebra in Computer Science},
  year = {2011},
  editor = {Corradini, Andrea and Klin, Bartek and Cirstea, Corina},
  volume = {6859},
  series = {Lecture Notes in Computer Science},
  pages = {70 -- 84},
  publisher = {Springer, Heidelberg},
  owner = {csfnf},
  timestamp = {2011.05.10}
}

@INPROCEEDINGS{backhouse1988meaning,
  author = {Roland Backhouse},
  title = {On the meaning and construction of the rules in {M}artin-{L}\"of's
	theory of types},
  booktitle = {Proceedings of the Workshop on general logic, Edinburgh, February,
	1987},
  year = {1988},
  editor = {Avron, A. and Harper, R. and Honsell, F. and Mason, I. and Plotkin,
	G.},
  volume = {ECS-LFCS-88-52},
  file = {:ECS-LFCS-88-52.pdf:PDF},
  owner = {csfnf},
  timestamp = {2010.01.07}
}

@ARTICLE{backhouse1989diytt,
  author = {Roland Backhouse and Paul Chisholm and Grant Malcolm and Erik Saaman},
  title = {{Do-it-yourself} type theory},
  journal = {Formal Aspects of Computing},
  year = {1989},
  volume = {1},
  pages = {19--84},
  number = {1},
  file = {:backhouse1989diytt.pdf:PDF},
  owner = {csfnf},
  publisher = {Springer},
  timestamp = {2010.01.07}
}

@ARTICLE{chapman2009eatitself,
  author = {James Chapman},
  title = {Type theory should eat itself},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = {2009},
  volume = {228},
  pages = {21--36},
  file = {:chapman2009eatitself.pdf:PDF},
  owner = {csfnf},
  publisher = {Elsevier},
  timestamp = {2010.01.07}
}

@INPROCEEDINGS{mcbride2010levitation,
  author = {James Chapman and Pierre-{\'E}variste Dagand and Conor McBride and
	Peter Morris},
  title = {The Gentle Art of Levitation},
  booktitle = {ICFP},
  year = {2010},
  volume = {45},
  number = {9},
  pages = {3--14},
  organization = {ACM},
  file = {:mcbride2010levitation.pdf:PDF},
  owner = {csfnf},
  timestamp = {2010.04.19}
}

@BOOK{conway2001ONAG,
  title = {On numbers and games},
  publisher = {AK Peters},
  year = {2001},
  author = {John Conway},
  owner = {Fredrik Forsberg},
  timestamp = {2011.07.31}
}

@MISC{coq,
  author = {{Coq team}, The},
  title = {Coq},
  howpublished = {{\tt http://coq.inria.fr/}},
  year = {2012},
  owner = {csfnf},
  timestamp = {2010.06.08}
}

@ARTICLE{danielsson2007formalisation,
  author = {Danielsson, Nils Anders},
  title = {A formalisation of a dependently typed language as an inductive-recursive
	family},
  journal = {Lecture Notes in Computer Science},
  year = {2007},
  volume = {4502},
  pages = {93--109},
  file = {:danielsson2007formalisation.pdf:PDF},
  owner = {csfnf},
  publisher = {Springer},
  timestamp = {2010.01.07}
}

@ARTICLE{dybjer2000IR,
  author = {Dybjer, Peter},
  title = {A general formulation of simultaneous inductive-recursive definitions
	in type theory},
  journal = {Journal of Symbolic Logic},
  year = {2000},
  volume = {65},
  pages = {525--549},
  number = {2},
  file = {:dybjer2000IR.pdf:PDF},
  owner = {csfnf},
  publisher = {The Association for Symbolic Logic, Inc.},
  timestamp = {2010.01.07}
}

@ARTICLE{dybjer1994indfam,
  author = {Dybjer, Peter},
  title = {Inductive families},
  journal = {Formal aspects of computing},
  year = {1994},
  volume = {6},
  pages = {440--465},
  number = {4},
  file = {:dybjer1994indfam.pdf:PDF},
  owner = {csfnf},
  publisher = {Springer},
  timestamp = {2010.01.07}
}

@ARTICLE{dybjersetzer2006IIR,
  author = {Dybjer, Peter and Setzer, Anton},
  title = {Indexed induction--recursion},
  journal = {Journal of logic and algebraic programming},
  year = {2006},
  volume = {66},
  pages = {1--49},
  number = {1},
  file = {:dybjersetzer2006IIR.pdf:PDF},
  owner = {csfnf},
  publisher = {Elsevier},
  timestamp = {2010.01.07}
}

@ARTICLE{dybjersetzer2003inalg,
  author = {Dybjer, Peter and Setzer, Anton},
  title = {Induction--recursion and initial algebras},
  journal = {Annals of Pure and Applied Logic},
  year = {2003},
  volume = {124},
  pages = {1--47},
  number = {1-3},
  file = {:dybjersetzer2003inalg.pdf:PDF},
  owner = {csfnf},
  publisher = {Elsevier},
  timestamp = {2010.01.07}
}

@CONFERENCE{dybjersetzer1999finax,
  author = {Dybjer, Peter and Setzer, Anton},
  title = {A Finite Axiomatization of Inductive-Recursive Definitions},
  booktitle = {Typed lambda calculi and applications: 4th international conference,
	TLCA'99, L'Aquila, Italy, April 7-9, 1999: proceedings},
  year = {1999},
  pages = {129--146},
  publisher = {Springer Verlag},
  file = {:dybjerSetzer1999finiteAx.pdf:PDF},
  owner = {csfnf},
  timestamp = {2010.01.06}
}

@UNPUBLISHED{ghaniHancock2012algIR,
  author = {Ghani, Neil and Hancock, Peter},
  title = {Containers, Monads and Induction Recursion},
  note = {To appear in MSCS},
  year = {2012},
  file = {:ghaniHancock2012algIR.pdf:PDF},
  owner = {csfnf},
  timestamp = {2012.02.27}
}

@INPROCEEDINGS{mamane2004surrealCoq,
  author = {Lionel Mamane},
  title = {Surreal Numbers in {Coq}},
  booktitle = {Types for Proofs and Programs: International Workshop TYPES 2004},
  year = {2006},
  editor = {Filliâtre, Jean-Christophe and Paulin-Mohring, Christine and Werner,
	Benjamin},
  volume = {3839},
  series = {Lecture Notes in Computer Science},
  pages = {170 -- 185},
  publisher = {Springer},
  file = {:mamane2004surrealCoq.pdf:PDF},
  owner = {csfnf},
  timestamp = {2011.10.04}
}

@BOOK{martinlof1984bibliopolis,
  title = {Intuitionistic type theory},
  publisher = {Bibliopolis Naples},
  year = {1984},
  author = {Martin-L{\"o}f, Per},
  file = {:martinlof1984bibliopolis.pdf:PDF},
  owner = {csfnf},
  timestamp = {2010.01.07}
}

@PHDTHESIS{morris2007thesis,
  author = {Peter Morris},
  title = {Constructing Universes for Generic Programming},
  school = {University of Nottingham},
  year = {2007},
  file = {:morris2007thesis.pdf:PDF},
  owner = {csfnf},
  timestamp = {2010.05.24}
}

@ARTICLE{morrisAltenkirchGhani2009SPFjournal,
  author = {Morris, Peter and Altenkirch, Thorsten and Ghani, Neil},
  title = {A universe of strictly positive families},
  journal = {International Journal of Foundations of Computer Science},
  year = {2009},
  volume = {20},
  pages = {83--107},
  number = {1},
  file = {:morrisAltenkirchGhani2009SPFjournal.pdf:PDF},
  owner = {csfnf},
  timestamp = {2012.02.27}
}

@ARTICLE{morrisAltenkirchMcBride2006regularTreeTypes,
  author = {Morris, Peter and Altenkirch, Thorsten and McBride, Conor},
  title = {Exploring the regular tree types},
  journal = {Types for Proofs and Programs},
  year = {2006},
  pages = {252--267},
  file = {:morrisAltenkirchMcBride2006regularTreeTypes.pdf:PDF},
  owner = {csfnf},
  publisher = {Springer},
  timestamp = {2012.02.27}
}

@INPROCEEDINGS{nordvallforsbergSetzer2010indind,
  author = {Nordvall Forsberg, Fredrik and Setzer, Anton},
  title = {Inductive-Inductive Definitions},
  booktitle = {Computer Science Logic},
  year = {2010},
  editor = {Dawar, Anuj and Veith, Helmut},
  volume = {6247},
  series = {Lecture Notes in Computer Science},
  pages = {454-468},
  publisher = {Springer Berlin / Heidelberg},
  affiliation = {Swansea University},
  file = {nordvallforsbergSetzer2010indind.pdf:nordvallforsbergSetzer2010indind.pdf:PDF},
  owner = {csfnf},
  timestamp = {2011.02.03}
}

@PHDTHESIS{norell2007thesis,
  author = {Ulf Norell},
  title = {Towards a practical programming language based on dependent type
	theory},
  school = {Department of Computer Science and Engineering, Chalmers University
	of Technology},
  year = {2007},
  file = {:norell2007thesis.pdf:PDF},
  owner = {csfnf},
  timestamp = {2010.01.07}
}

@comment{jabref-meta: selector_publisher:}

@comment{jabref-meta: selector_author:}

@comment{jabref-meta: selector_journal:}

@comment{jabref-meta: selector_keywords:}