notes.bib

@STRING{lfcs    = "{L}{F}{C}{S}, {U}niversity
                  of {E}dinburgh" }
@STRING{jfp     = "{JFP}" }
@STRING{dtp08 = "{DTP}'08" }
@STRING{brunosmiddlenames = "" }
@STRING{wgp = "{WGP}"}
@STRING{subm = "Submitted"}


@inproceedings{DBLP:conf/afp/Norell08,
  author    = {Ulf Norell},
  title     = {Dependently Typed Programming in Agda},
  booktitle = {Advanced Functional Programming},
  year      = {2008},
  pages     = {230-266},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04652-0_5},
  crossref  = {DBLP:conf/afp/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/afp/2008,
  editor    = {Pieter W. M. Koopman and
               Rinus Plasmeijer and
               S. Doaitse Swierstra},
  title     = {Advanced Functional Programming, 6th International School,
               AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures},
  booktitle = {Advanced Functional Programming},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5832},
  year      = {2009},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04652-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{deBruijn:dummies,
  author = 	 {Nicolas G. de~Bruijn},
  title = 	 "{Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation}",
  journal = 	 {Indagationes Mathematic{\ae}},
  year = 	 {1972},
  OPTkey = 	 {},
  volume =	 {34},
  OPTnumber = 	 {},
  pages =	 {381--392},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{         burstall:induction,
  author        = "Rod Burstall",
  title         = "Proving Properties of Programs by Structural Induction",
  journal       = "Computer {J}ournal",
  year          = "1969",
  volume        = "12",
  number        = "1",
  pages         = "41--48",
  OPTmonth         = feb
}

@Article{         burstall:inductively,
  author        = "Rod Burstall",
  title         = "{I}nductively {D}efined {F}unctions in {F}unctional
		  {P}rogramming {L}anguages",
  journal       = "Journal of Computer and System Sciences",
  year          = "1987",
  volume        = "34",
  pages         = "409--421"
}
@inproceedings{mcbride:free_variable,
    author = {McBride, Conor and Mckinna, James},
    booktitle = {Haskell '04},
    pages = {1--9},
    publisher = {ACM},
    title = {Functional pearl: i am not a number--i am a free variable},
    year = {2004}
}

@article{conor.james:viewfromleft,
   journal = {Journal of Functional Programming},
   number = {1},
   volume = {14},
   title = {The View From The Left},
   year = {2004},
   author = {Conor McBride and James McKinna}
}

@incollection{dybjer:nbe,
    author = {Dybjer, Peter and Filinski, Andrzej},
    journal = {Applied Semantics},
    pages = {75--114},
    title = {Normalization and Partial Evaluation},
    year = {2002}
}

@incollection{dybjer:dependent_types_work,
    author = {Bove, Ana and Dybjer, Peter},
    journal = {Language Engineering and Rigorous Software Development},
    pages = {57--99},
    title = {Dependent Types at Work},
    year = {2009}
}

@phdthesis{chapman:phd,
    author = {Chapman, James},
    school = {University of Nottingham},
    title = {Type checking and normalisation}
}

@inproceedings{chapman:ett,
    author = {Chapman, James and Altenkirch, Thorsten and Mcbride, Conor},
    booktitle = {6th Symposium on Trends in Functional Programming},
    location = {Tallinn, Estonia},
    month = {September},
    title = {Epigram reloaded: a standalone typechecker for ETT},
    year = {2005}
}

@inproceedings{turner:bidirectional_tc,
    address = {New York, NY},
    author = {Pierce, Benjamin C. and Turner, David N.},
    booktitle = {POPL'98},
    pages = {252--265},
    title = {Local Type Inference},
    year = {1998}
}

@TechReport{boutillier:report,
  author = 	 {Boutillier, Pierre},
  title = 	 {Equality for $\lambda$-terms with list primitives},
  institution =  {Ecole Normale Superieure de Lyon},
  year = 	 {2009},
  url = {http://perso.ens-lyon.fr/pierre.boutillier/files/Boutillier09.pdf}
}

@inproceedings{morris:spf,
    author = {Morris, Peter and Altenkirch, Thorsten and Ghani, Neil},
    booktitle = {CATS '07},
    pages = {111--121},
    publisher = {Australian Computer Society, Inc.},
    title = {Constructing strictly positive families},
    year = {2007}
}

@unpublished{mcbride:ornaments,
    author = {Mcbride, Conor},
    title = {Ornamental Algebras, Algebraic Ornaments}
}

@incollection{dybjer:ir_axiom,
    author = {Dybjer, Peter and Setzer, Anton},
    journal = {Typed Lambda Calculi and Applications},
    pages = {643},
    title = {A Finite Axiomatization of Inductive-Recursive Definitions},
    year = {1999}
}

@inproceedings{dybjer:ir_algebra,
    author = {Dybjer, Peter and Setzer, Anton},
    booktitle = {Annals of Pure and Applied Logic},
    title = {Induction-Recursion and Initial Algebras},
    volume = {124},
    year = {2000}
}

@incollection{dybjer:iir,
    author = {Dybjer, Peter and Setzer, Anton},
    journal = {Proof Theory in Computer Science},
    pages = {93--113},
    title = {Indexed Induction-Recursion},
    year = {2001}
}

@inproceedings{mcbride:motive,
 author = {McBride, Conor},
 title = {Elimination with a Motive},
 booktitle = {TYPES '00},
 year = {2002},
 }

@unpublished{hancock:amen,
    author = {Hancock, Peter},
    title = {AMEN: the last word in combinators}
}

@article{huet:zipper,
 author = {Huet, G\'{e}rard},
 title = {The Zipper},
 journal = {J. Funct. Program.},
}

@incollection{mcbride:pattern_matching,
    author = {Goguen, Healfdene and McBride, Conor and McKinna, James},
    booktitle = {Algebra, Meaning and Computation },
    title = {Eliminating Dependent Pattern Matching},
    year = {2006}
}

@inproceedings{altenkirch_mcbride_swierstra:obs_equality,
    author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
    title = {Observational equality, now!},
    booktitle = {PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification},
    year = {2007},    
    pages = {57--68},
    location = {Freiburg, Germany},
 }

@inproceedings{DBLP:conf/csl/AltenkirchR99,
  author    = {Thorsten Altenkirch and
               Bernhard Reus},
  title     = {Monadic Presentations of Lambda Terms Using Generalized
               Inductive Types},
  booktitle = {CSL},
  year      = {1999},
  pages     = {453-468},
  ee        = {http://dx.doi.org/10.1007/3-540-48168-0_32},
  crossref  = {DBLP:conf/csl/1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/csl/1999,
  editor    = {J{\"o}rg Flum and
               Mario Rodr\'{\i}guez-Artalejo},
  title     = {Computer Science Logic, 13th International Workshop, CSL
               '99, 8th Annual Conference of the EACSL, Madrid, Spain,
               September 20-25, 1999, Proceedings},
  booktitle = {CSL},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1683},
  year      = {1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{conor.ross:applicative.functors,
  author = 	 {Conor McBride and Ross Paterson},
  title = 	 {Applicative programming with effects},
  journal =      jfp,
  year =	 2008
}


@InProceedings{wadler:views,
  author = 	 "Philip Wadler",
  title = 	 "Views: A way for pattern matching to cohabit with
		  data abstraction",
    crossref =	 "popl87",
}


@Proceedings{     popl87,
  key           = "POPL'87",
  title         = "14th {A}nnual {S}ymposium on Principles of {P}rogramming {L}anguages
                  (POPL) (Munich)",
  booktitle     = "Proceedings of {POPL} '87",
  organization  = "ACM",
  OPTmonth         = jan,
  year          = 1987,
  crossrefonly  = 1
}