text:
@STRING{jfp     = "{Journal of Functional Programming}" }
@STRING{jar     = "{Journal of Automated Reasoning}" }
@STRING{jsc     = "{Journal of Symbolic Computation}" }
@STRING{tcs     = "{Theoretical Computer Science}" }
@String{sv      = {Springer-Verlag}}
@STRING{fac     = "{F}ormal {A}spects of {C}omputing" }
@STRING{icfp    = "{ACM} {I}nternational {C}onference on {F}unctional {P}rogramming" }
@STRING{lfcs    = "{L}aboratory for {F}oundations of {C}omputer {S}cience, {U}niversity
                  of {E}dinburgh" }
@STRING{mfps    = "{M}athematical {F}oundations of {P}rogramming {S}emantics" }
@STRING{lncs    = "{LNCS}" }
@STRING{popl    = "Annual Symposium on Principles of Programming Languages
                  (POPL)" }

@inproceedings{pierce.vouillon.hosoya:regular.expression.types,
    author = "Haruo Hosoya and J\'er\^ome Vouillon and Benjamin C. Pierce",
    title = "{R}egular {E}xpression {T}ypes for {XML}",
    booktitle = "Proceedings of the {I}nternational {C}onference on {F}unctional {P}rogramming",
    year = "2000"
}

@inproceedings{baars.swierstra:selfinspecting,
  author = {Arthur I. Baars and S. Doaitse Swierstra},
  title = {Type Safe, Self Inspecting Code},
  crossref={hw2004}
}

@inproceedings{oleg.ralf.keean:hlists,
  author={Oleg Kiselyov and Ralf L\"{a}mmel and Keean Schupke},
  title={Strongly {T}yped {H}eterogeneous {C}ollections},
  crossref={hw2004}
}

@inproceedings{bringert.hockersten:haskellDB,
  author={Bj\"{o}rn Bringert and Anders H\"ockersten},
  title={Haskell{DB} {I}mproved},
  crossref={hw2004}
}

@article{thiemann:programmabletypes,
  author={Peter Thiemann},
  title={Programmable Type Systems for Domain Specific Languages},
  journal={Electronic Notes in Theoretical Computer Science},
  volume={76},
  year={2002}
}

@inproceedings{kent-refactoring,
author = {Huiqing Li and Claus Reinke and Simon Thompson},
title = {Tool Support for Refactoring Functional Programs},
month = {August},
year = {2003},
pages = {},
keywords = {refactoring functional programs tool Haskell Strafunski Programatica},
note = {ISBN 1-58113-758-3},
url = {http://www.cs.kent.ac.uk/pubs/2003/1677},
publication_type = {inproceedings},
submission_id = {23380_1060161103},
booktitle = {ACM SIGPLAN 2003 Haskell Workshop },
editor = {Johan Jeuring},
organization = {Association for Computing Machinery},
refereed = {Refereed},
}

@Article{paul.zhaohui:coercions.universes,
  author = 	 {Paul Callaghan and Zhaohui Luo},
  title = 	 {An Implementation of {LF} with Coercive Subtyping \&
                  Universes},
  journal = 	 jar,
  year = 	 2001,
  volume =	 27,
  pages =	 {3--27}
}

@InProceedings{   luo:coercive,
  author        = "Zhaohui Luo",
  title         = "Coercive Subtyping in Type Theory",
  crossref      = "lncs1258",
  pages         = "275--296"
}

@InProceedings{   damas.milner:principal,
  author        = "Luis Damas and Robin Milner",
  title         = "Principal Type-Schemes for Functional Programming
                  Languages",
  crossref      = "popl82",
  pages         = "207-212"
}

@InProceedings{magnusson.nordstrom:alf,
  author = 	 {Lena Magnusson and Bengt Nordstr\"{o}m},
  title = 	 {The {ALF} proof editor and its proof engine},
  crossref =  {lncs806},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{wadler.blott:less.ad.hoc,
  author = 	 {Philip Wadler and Stephen Blott},
  title = 	 {How to make ad-hoc polymorphism less ad hoc},
  booktitle = 	 {16th {ACM} {S}ymposium on {P}rinciples of {P}rogramming
                  {L}anguages},
  pages =	 "60--76",
  year =	 1989,
  month =	 jan,
  publisher =	 {{ACM}}
}

@InProceedings{edwin.conor.james:family.indices,
  author = 	 {Edwin Brady and Conor McBride and James McKinna},
  title = 	 {Inductive Families Need Not Store Their Indices},
  booktitle = 	 {Types for Proofs and Programs, Torino, 2003},
  pages =	 {115-129},
  year =	 2004,
  editor =	 {Stefano Berardi and Mario Coppo and Ferrucio Damiani},
  volume =	 3085,
  series =	 lncs,
  publisher =	 sv
}

@Book{coqart,
  author =	 {Yves Bertot and Pierre Cast\'{e}ran},
  title = 	 {{I}nteractive {T}heorem {P}roving and
                  {P}rogram {D}evelopment,
                  {C}oq'{A}rt:
                  {T}he {C}alculus of {I}nductive {C}onstructions},
  publisher = 	 sv,
  year = 	 2004,
  series =	 {{T}exts in {T}heoretical {C}omputer {S}cience}
}

@phdthesis{edwin:thesis,
  author = "Edwin Brady",
  title = "{P}ractical {I}mplementation of a {D}ependently {T}yped {F}unctional
{P}rogramming {L}anguage",
  school = "University of Durham",
  year = 2005
}

@Article{laemmel.peytonjones:boilerplate,
  author =       "Ralf L{\"a}mmel and Simon {Peyton Jones}",
  title =        "Scrap your boilerplate: a practical design pattern for
                 generic programming",
  journal =      "ACM SIG{\-}PLAN Notices",
  volume =       "38",
  number =       "3",
  pages =        "26--37",
  month =        mar,
  year =         "2003",
  note = "Proc.\ of the ACM SIGPLAN Workshop
          on Types in Language Design and Implementation (TLDI~2003)"
}

@inproceedings{laemmel.peytonjones:moreboilerplate,
  author    = "Ralf L{\"a}mmel and Simon {Peyton Jones}",
  title     = "Scrap more boilerplate: reflection, zips, and generalised casts",
  booktitle = "Proceedings; International Conference on Functional Programming (ICFP 2004)",
  year      = "2004",
  month     = sep,
  publisher = "ACM Press",
  note      = "To appear"
}

@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 = 	 {}
}

@book{Okasaki,
   title = {Purely Functional Data Structures},
   year = {1998},
   publisher = {Cambridge University Press},
   author = {Chris Okasaki}
}

@techreport{xi-imp,
   title = {Imperative Programming with Dependent Types},
   year = {2000},
   institution = {University of Cincinnati},
   author = {Hongwei Xi}
}

@misc{michael:dtal,
   title = {A Dependently Typed Assembly Language},
   year = {1999},
   author = {Hongwei Xi and Robert Harper}
}

@article{hughes-matters,
   journal = {Computer Journal},
   number = {2},
   volume = {32},
   title = {Why Functional Programming Matters},
   year = {1989},
   pages = {98--107},
   author = {J. Hughes}
}

@Book{sml:definition,
  author =	 {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
  ALTeditor = 	 {},
  title = 	 {The {Definition} of {Standard ML}, revised edition},
  publisher = 	 {{MIT Press}},
  year = 	 {1997},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{sml:commentary,
  author =	 {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
  ALTeditor = 	 {},
  title = 	 {The {Commentary} on {Standard ML}},
  publisher = 	 {{MIT Press}},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@TechReport{genHaskell,
  author = 	 {Dave Clarke and Ralf Hinze and Johan Jeuring and Andres L\"{o}h and Jan de Wit},
  title = 	 {The {Generic Haskell} user's guide},
  institution =  {Utrecht University},
  year = 	 {2001},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {UU-CS-2001-26},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{leijer.meijer:phants-on-fire,
  author = 	 {Daan Leijen and Erik Meijer},
  title = 	 {Domain specific embedded compilers},
  booktitle = 	 "{2nd Conference on Domain-Specific Languages (DSL)}",
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {1999},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {Austin TX, USA},
  OPTmonth = 	 {October },
  organization = {USENIX},
  OPTpublisher = {},
  note =	 {Available from \url{http://www.cs.uu.nl/people/daan/papers/dsec.ps}},
  OPTannote = 	 {}
}

@InProceedings{tamaki.sato:fold-unfold,
  author = 	 {Hisao Tamaki and Taisuke Sato},
  title = 	 {Unfold/fold transformation of logic programs},
  booktitle = 	 "{Proceedings 2nd International Logic Programming Conference}",
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {127--138},
  year =	 {1984},
  editor =	 "{Sten-{\AA}ke T{\aa}rnlund}",
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InCollection{clark:completion,
  author = 	 {Keith Clark},
  title = 	 {Negation as failure},
  booktitle = 	 {Logic and data bases},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {292-322},
  publisher =	 {Plenum Press},
  year =	 {1978},
  editor =	 "{Herv{\'e} Gallaire and Jack Minker}",
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{ severi.poll:defs,
  author = 	 {Paula Severi and Erik Poll},
  title = 	 "{Pure Type Systems with definitions}",
  booktitle = 	 "{Proceedings of LFCS'94}",
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {316--328},
  year =	 {1994},
  editor =	 "{Anil Nerode and Yuri Matijasevi{\v{c}}}",
  volume =	 {813},
  OPTnumber = 	 {},
  series =	 lncs,
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 sv,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@phdthesis{xi-thesis,
   OPTmonth = {December},
   school = {Department of Mathematical Sciences, Carnegie Mellon University},
   title = {Dependent Types in Practical Programming},
   year = {1998},
   author = {Hongwei Xi}
}

@Unpublished{roorda.jeuring:pts.fp,
  author =       {Jan-Willem Roorda and Johan Jeuring},
  title =        {Pure Type Systems for Functional Programming},
  note =         {In preparation},
  year =         2001
}

@InProceedings{altenkirch:extensional,
  author =       {Thorsten Altenkirch},
  title =        {Extensional Equality in Intensional Type Theory},
  booktitle =    {{LICS} 99},
  year =         1999
}

@PhDThesis{       hofmann:thesis,
  author        = "Martin Hofmann",
  title         = "Extensional concepts in intensional type theory",
  school        = lfcs,
  year          = 1995,
  note           = "Available from \url{http://www.lfcs.informatics.ed.ac.uk/reports/95/ECS-LFCS-95-327/}"

}

@Article{abel.altenkirch:structural.recursion,
  author = 	 {Andreas Abel and Thorsten Altenkirch},
  title = 	 {A Predicative Analysis of Structural Recursion},
  journal = 	 jfp,
  year = 	 2000,
  OPTmonth =	 {March}
}

@InProceedings{altenkirch.reus:monads.lambda,
  author = 	 "Thorsten Altenkirch and Bernhard Reus",
  title = 	 "Monadic presentations of lambda-terms using
		  generalized inductive types",
  booktitle =	 "{C}omputer {S}cience {L}ogic 1999",
  year =	 1999
}

@Article{mckinna.pollack:formal.lambda,
  author = 	 "James McKinna and Robert Pollack",
  title = 	 "Some Lambda Calculus and Type Theory Formalized",
  journal =	 jar,
  year =	 1999,
  volume =	 23,
  pages =	 "373--409",
  note =	 "(Special Issue on Formal Proof, editors Gail Pieper and
		  Frank Pfenning)"
}

@InProceedings{mckinna.pollack:pts,
  author = 	 {James McKinna and Robert Pollack},
  title = 	 {Pure Type Systems Formalized},
  crossref =  {lncs664},
  OPTkey = 	 {},
  OPTpages = 	 {},
  OPTvolume = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{jutting-mckinna-pollack,
  author = 	 {Bert van~Benthem~ Jutting and James McKinna and Robert Pollack},
  title = 	 {Checking {Algorithms for Pure Type Systems}},
  crossref =  {lncs806},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{mckinna-mcbride:views.for.recursion,
  OPTkey = 	 {},
  author =	 {James McKinna},
  title =	 {Views for recursion},
  howpublished = {Talk given at the workshop on {T}ermination and {T}ype {T}heory, Hind{\aa}s, Sweden},
  OPTmonth =	 nov,
  year =	 2002,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{mcbride-mckinna:seeing.and.doing,
  OPTkey = 	 {},
  author =	 {Conor McBride},
  title =	 {Seeing and Doing},
  howpublished = {Talk given at the workshop on {T}ermination and {T}ype {T}heory, Hind{\aa}s, Sweden},
  OPTmonth =	 nov,
  year =	 2002,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{voda:clausal.language.talk,
  OPTkey = 	 {},
  author =	 {Paul Voda},
  title =	 {What do we gain by integrating a Programming Language with a Theorem Prover?},
  howpublished = {Talk given at the workshop on {T}ermination and {T}ype {T}heory, Hind{\aa}s, Sweden},
  OPTmonth = 	 nov,
  year =	 2002,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Unpublished{voda:clausal.language.paper,
  author = 	 {Paul Voda},
  title = 	 {},
  note = 	 {},
  OPTkey = 	 {},
  OPTmonth = 	 {},
  year =	 {2002},
  OPTannote = 	 {}
}

@InCollection{bundy:induction,
  author = 	 {Alan Bundy},
  title = 	 {{T}he {A}utomation {O}f {P}roof {B}y {M}athematical {I}nduction},
  booktitle = 	 {{H}andbook of {A}utomated {R}easoning},
  publisher =	 {Elsevier Science},
  year =	 1999,
  editor =	 {Alan Robinson and Andrei Voronkov}
}

@Misc{paulin:habilitation,
  author =       {Christine Paulin-Mohring},
  title =        {D\'{e}finitions {I}nductives
  en {T}h\'eorie des {T}ypes d'{O}rdre {S}up\'{e}rieur},
  howpublished = {Habilitation Thesis.
  {U}niversit\'{e} {C}laude {B}ernard ({L}yon I)},
  year =         1996
}

@Misc{streicher:habilitation,
  author =       {Thomas Streicher},
  title =        {Investigations into intensional
  type theory},
  howpublished = {Habilitation Thesis, {L}udwig {M}aximilian
                      {U}niversit\"{a}t},
  year =         1993
}

@InProceedings{hofmann.streicher:groupoid,
  author =	 {Martin Hofmann and Thomas Streicher},
  title =	 {A groupoid model refutes uniqueness of identity
                  proofs},
  booktitle =	 "{Proc. Ninth Annual Symposium on Logic in Computer
                  Science (LICS) (Paris, France)}",
  pages =	 {208--212},
  year =	 1994,
  publisher =	 "{IEEE Computer Society Press}"
}

@Unpublished{     martinloef:atheoryoftypes,
  author        = "Per Martin-L{\"o}f",
  title         = "A Theory of Types",
  note          = "manuscript",
  year          = "1971"
}

@Book{            martinloef:intuitionistic,
  author        = "Per Martin-L{{\"o}f}",
  title         = "Intuitionistic Type Theory",
  publisher     = "Bibliopolis$\cdot$Napoli",
  year          = 1984
}

@Misc{coq:7.0,
  author =	 "L'{\'E}quipe Coq",
  title =	 "The {C}oq {P}roof {A}ssistant {R}eference {M}anual",
  howpublished = "\url{http://pauillac.inria.fr/coq/doc/main.html}",
  year =	 2001,
  OPTmonth =	 "Apr"
}

@InProceedings{   coquand.paulin:inductively,
  author        = "Thierry Coquand and Christine Paulin",
  title         = "Inductively Defined Types",
  crossref      = "lncs417",
  pages         = "50--66"
}

@Article{miller:beta0.unification,
  author =       {Dale Miller},
  title =        {A {L}ogic {P}rogramming {L}anguage with
  {L}ambda-{A}bstraction, {F}unction {V}ariables and {S}imple {U}nification},
  journal =      { Journal of
  {L}ogic and {C}omputation},
  year =         1991,
  volume =       2,
  number =       4,
  pages =        {497--537}
}

@Article{schuermann.despeyroux.pfenning:primrec.hoas,
  author = 	 {Carsten Sch{\"u}rmann and Joelle Despeyroux and
                  Frank Pfenning},
  title = 	 {Primitive recursion for higher-order abstract syntax},
  journal = 	 tcs,
  year = 	 2000,
  note =	 {To appear}
}

@Article{ pfenning.elliott:hoas,
    author = "Frank Pfenning and Conal Elliott",
    title = "Higher-Order Abstract Syntax",
    booktitle = "Proceedings of the {ACM} {SIGPLAN} '88 Conference on Programming Language Design and Implementation ({PLDI})",
    journal = "SIGPLAN Notices",
    volume = "23",
    number = "7",
    pages = "199--208",
    year = "1988"
}

@PhdThesis{cornes:phd,
  author = 	 "Cristina Cornes",
  title = 	 "Conception d'un langage de haut niveau de
		  r{\'e}presentation de preuves",
  school = 	 "Universit{\'e} Paris VII",
  year = 	 1997
}

@PhDThesis{       mckinna:thesis,
  author        = "James McKinna",
  title         = "Deliverables: A Categorical Approach to Program
                  Development in Type Theory",
  school        = lfcs,
  year          = 1992,
  url           = "\url{ftp://ftp.dcs.ed.ac.uk/pub/jhm/thesis.ps.gz}"
}

@PhDThesis{       healf:thesis,
  author        = "Healfdene Goguen",
  title         = "{A} {Typed} {Operational} {Semantics} for {Type} {Theory}",
  school        = lfcs,
  year          = 1994,
  note           = "Available from \url{http://www.lfcs.informatics.ed.ac.uk/reports/94/ECS-LFCS-94-304/}"
}

@InProceedings{gimenez:structural.recursion,
  author = 	 "Eduardo Gim{\'e}nez",
  title = 	 "{Structural Recursive Definitions in
                  Type Theory}",
  booktitle =	 "{Proceedings of ICALP '98}",
  series =	 lncs,
  volume =       1443,
  year =	 1998,
  publisher =	 sv,
  OPTmonth =	 "July"
}

@Article{debruijn:telescopes,
  author = 	 {Nicolas G. de~{B}ruijn},
  title = 	 {{T}elescopic {M}appings in {T}yped
  {L}ambda-{C}alculus},
  journal = 	 {Information and Computation},
  year = 	 1991,
  volume =	 91,
  pages =	 {189--204}
}

@InProceedings{gimenez:guarded.fixpoint,
  author = 	 "Eduardo Gim{\'e}nez",
  title = 	 "Codifying guarded definitions with
  recursive schemes",
  crossref =     "lncs996",
  pages =	 "39--59"
}

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

@InProceedings{wadler:theoremsforfree,
  author = 	 "Philip Wadler",
  title = 	 "{Theorems for Free!}",
  crossref =	 "fpca89",
}

@Article{         miller:mixed,
  author        = "Dale Miller",
  title         = "Unification under a Mixed Prefix",
  journal       = jsc,
  year          = 1992,
  volume        = 14,
  number        = 4,
  pages         = "321-358"
}

@Article{conor:faking,
  author = 	 {Conor McBride},
  title = 	 {{F}aking {I}t
                  ({S}imulating {D}ependent {T}ypes in {H}askell)},
  journal = 	 jfp,
  year = 	 {2002},
  OPTkey = 	 {},
  volume =	 {12},
  number =	 {4\& 5},
  pages =	 {375--392},
  OPTmonth = 	 {},
  note =	 {{S}pecial {I}ssue on {H}askell},
  OPTannote = 	 {}
}

@InProceedings{conor:motive,
  author =       {Conor McBride},
  title =        {{E}limination with a {M}otive},
  crossref =     {clmp:types00}
}

@Unpublished{     pollack:implicit,
  author        = "Robert Pollack",
  title         = "Implicit Syntax",
  note          = "{Available from \url{ftp://ftp.dcs.ed.ac.uk/pub/lego/ImplicitSyntax.ps.Z}. An earlier version of this paper appeared in
                  \cite{lfworkshop90}}",
  year          = 1992,
  OPTmonth         = may,
  url           = "\url{ftp://ftp.dcs.ed.ac.uk/pub/lego/ImplicitSyntax.ps.Z}"
}

@Article{conor:unification,
  author = 	 {Conor McBride},
  title = 	 {{F}irst-{O}rder {U}nification by {S}tructural
                  {R}ecursion},
  journal = 	 jfp,
  year = 	 {2003},
  volume =	 {13},
  number =	 {6},
  pages =	 {1061--1075},
  month = 	 {dec}
}

@InProceedings{cornes.terrasse:inversion,
  author = 	 {Cristina Cornes and Delphine Terrasse},
  title = 	 {{I}nverting {I}nductive {P}redicates in {C}oq},
  crossref =  {lncs1158},
}

@InProceedings{   conor:inversion,
  author        = "Conor McBride",
  title         = "Inverting Inductively Defined Relations in {LEGO}",
  crossref =	 "lncs1512",
  pages =	 "236--253"
}

@InProceedings{   coquand:patternmatching,
  author        = {Thierry Coquand},
  title         = {Pattern {M}atching with {D}ependent {T}ypes},
  crossref      = "lfworkshop92"
}

@InProceedings{tullsen:zip.calculus,
  author = 	 "Mark Tullsen",
  title = 	 "The {Z}ip {C}alculus",
  crossref =	 "lncs1837",
  pages =	 "28--44"
}

@Article{         bellegarde.hook:substitution.monad,
  author        = "Francoise Bellegarde and James Hook",
  title         = "Substitution: {A} formal methods case study using monads
                  and transformations",
  year          = "1995",
  url           = "\url{ftp://cse.ogi.edu/pub/pacsoft/papers/substitution.ps.gz}",
  journal       = "{S}cience of {C}omputer {P}rogramming"
}

@Book{            luo:typetheoryforcs,
  author        = "Zhaohui Luo",
  title         = "{C}omputation and {R}easoning: {A} {T}ype {T}heory
		  for {C}omputer {S}cience",
  publisher     = "{O}xford {U}niversity {P}ress",
  year          = 1994
}

@PhdThesis{luo:ecc,
  author = 	 "Zhaohui Luo",
  title = 	 "{{ECC}: {An Extended Calculus of Constructions}}",
  school = 	 {University of Edinburgh},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  note =	 {Available from \url{http://www.lfcs.informatics.ed.ac.uk/reports/90/ECS-LFCS-90-118/}},
  OPTannote = 	 {}
}

@InProceedings{coquand.coquand:agda,
  author = 	 "Catarina Coquand and Thierry Coquand",
  title = 	 "Structured {T}ype {T}heory",
  booktitle =	 "Workshop on {L}ogical {F}rameworks and {M}etalanguages",
  year =	 1999
}

@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"
}

@PhdThesis{magnusson:phd,
  author = 	 "Lena Magnusson",
  title = 	 "The implementation of {ALF}---{A} {P}roof {E}ditor based
		  on {M}artin-{L}{\"o}f's {M}onomorphic {T}ype {T}heory with
		  {E}xplicit {S}ubstitution",
  school = 	 "Chalmers University of Technology, G{\"o}teborg",
  year = 	 1994
}

@Misc{hugs.manual2000,
  author = 	 "Mark P. Jones and John C. Peterson",
  title =	 "Hugs 98 {U}ser {M}anual",
  OPTmonth =	 {September},
  year =	 1999,
  note =	 {Available at \url{http://www.cse.ogi.edu/PacSoft/projects/Hugs/pages/downloading.htm}}
}

@Proceedings{haskell.report98,
  OPTauthor =       "Simon Peyton{~}Jones and John Hughes",
  editor = 	 "Simon Peyton{~}Jones and John Hughes",
  title =	 "Haskell'98: {A} {N}on-{S}trict {F}unctional {L}anguage",
  OPTmonth =	 feb,
  year =	 1999,
  note =	 {Available from \url{http://www.haskell.org/definition}}
}

@InProceedings{jones:fundeps,
  author = 	 "Mark P. Jones",
  title = 	 "Type {C}lasses with {F}unctional {D}ependencies",
  crossref =	 "lncs1782",
  pages =	 "230--244"
}

@InProceedings{peytonjones.jones.meijer:type.classes,
  author =	 "Simon Peyton{~}Jones and Mark Jones and Erik Meijer",
  title =	 "Type classes: an exploration of the design space",
  year =	 1997,
  booktitle = 	 {{P}roceedings of the {H}askell {W}orkshop},
  address =	 {{A}msterdam, {T}he {N}etherlands},
  OPTmonth =	 {June}
}

@InProceedings{hinze:polykinded,
  author = 	 "Ralf Hinze",
  title = 	 "Polytypic {V}alues {P}ossess {P}olykinded {T}ypes",
  crossref =	 "lncs1837",
  pages =	 "2--27"
}

@Article{bird.paterson:folds.nested,
  author = 	 "Richard Bird and Ross Paterson",
  title = 	 "Generalised folds for nested datatypes",
  journal =	 fac,
  volume =       11,
  year =	 1999,
  number =	 3
}

@InProceedings{pollack:records,
  author =       {Robert Pollack},
  title =        {Dependently {T}yped {R}ecords for {R}epresenting
                  {M}athematical {S}tructure},
  booktitle =    {{T}heorem {P}roving in {H}igher {O}rder {L}ogics,
                  {TPHOL}s 2000},
  year =         2000,
  editor =       {Mark Aagard and John Harrison},
  volume =       1869,
  OPTmonth =        aug,
  series        = lncs,
  publisher     = "Springer-Verlag"
}

@InProceedings{bove.capretta:nested.recursion,
  author =       "Ana Bove and Venanzio Capretta",
  title =        "{Nested General Recursion and Partiality in Type Theory}",
  booktitle =    "{{T}heorem {P}roving in {H}igher {O}rder {L}ogics,
                  {TPHOL}s 2001}",
  year =         2001,
  editor =       "{Richard Boulton and Paul Jackson}",
  volume =       2152,
  OPTmonth =        sep,
  series        = lncs,
  publisher     = "Springer-Verlag"
}

@InProceedings{   pfenning.paulinmohring:inductivetypes,
  author        = "Frank Pfenning and Christine Paulin-Mohring",
  title         = "Inductively {D}efined {T}ypes in the {C}alculus of
                  {C}onstructions",
  booktitle     = mfps # " 1989",
  editor        = "M. Main and A. Melton and M. Mislove and D. Schmidt",
  year =         1990,
  volume =       442,
  series        = lncs,
  publisher     = "Springer-Verlag",
  pages         = "209--228"
}

@Article{wadler:deforestation,
  author =       {Philip Wadler},
  title =        {Deforestation: transforming programs to eliminate trees},
  journal =      {Theoretical Computer Science},
  year =         {1990},
  volume =       {73},
  pages =        {231--248},
  note =         {(Special issue of selected papers from 2'nd ESOP.)}
}

@Misc{peytonjones.meijer:henk,
  author =	 "Simon Peyton{~}Jones and Erik Meijer",
  title =	 "Henk: a typed intermediate language",
  year =	 1997,
  note =	 "{ACM} {W}orkshop on {T}ypes in {C}ompilation."
}

@Unpublished{conor:derivative,
  author = 	 "Conor McBride",
  title = 	 "The {D}erivative of a {R}egular {T}ype is its {T}ype of
		  {O}ne-{H}ole {C}ontexts",
  note = 	 "{Available at \url{http://www.dur.ac.uk/c.t.mcbride/diff.ps}}",
  year =	 2001

}

@InProceedings{augustsson:compiling.patterns,
  author =       {Lennart Augustsson},
  title =        {{C}ompiling {P}attern {M}atching},
  crossref =     {lncs201},
  pages =        {368--381}
}

@InProceedings{hughes:lazy.memo,
  author =       {John Hughes},
  title =        {Lazy {M}emo-functions},
  crossref =     {lncs201},
  pages =        {129--146}
}

@InProceedings{hughes:garbage.collection,
  author =       {John Hughes},
  title =        "{A Distributed Garbage Collection Algorithm}",
  crossref =     {lncs201},
  pages =        {256--272}
}

@InProceedings{jonsson:lambda.lifting,
  author =       {Thomas J{o}hnsson},
  title =        "{Lambda Lifting: Transforming Programs to Recursive Equations}",
  crossref =     {lncs201},
  pages =        {190--203}
}

@InProceedings{wadler:failure.successes,
  author =       {Philip Wadler},
  title =        {How to {R}eplace {F}ailure by a {l}ist of {S}uccesses},
  crossref =     {lncs201},
  pages =        {113--128}
}

@Manual{mcbride.mcbride:craft89,
  title = 	 "Craft '89",
  author =	 "Fred McBride and Conor McBride",
  organization = "Queen's University, Belfast",
  year =	 1989,
  note =	 "User Manual"
}

@Unpublished{augustsson.carlsson:dependent.interpreter,
  author = 	 "Lennart Augustsson and Magnus Carlsson",
  title = 	 "An exercise in dependent types: A well-typed interpreter",
  note = 	 "{Available at \url{http://www.cs.chalmers.se/~augustss/cayenne/interp.ps}}",
  year =	 1999
}

@InProceedings{augustsson:cayenne,
  author = 	 "Lennart Augustsson",
  title = 	 "Cayenne---a language with dependent types",
  crossref =     "icfp98"
}

@Article{danvy:printf,
  author = 	 "Olivier Danvy",
  title = 	 "Functional Unparsing",
  journal =	 jfp,
  year =	 1998,
  volume =	 8,
  number =	 6,
  pages =	 "621--625",
  OPTmonth =	 nov
}

@Article{fridlender.indrika:zipwith,
  author = 	 "Daniel Fridlender and Mia Indrika",
  title = 	 "Do we need dependent types?",
  journal =	 "Journal of {F}unctional {P}rogramming",
  year =	 2000,
  volume =	 10,
  number =	 4,
  pages =	 "409--415",
  OPTmonth =	 "July",
  publisher     = "{CUP}"
}

@Article{huet:zipper,
  author = 	 "G\'{e}rard Huet",
  title = 	 "{T}he {Z}ipper",
  journal =	 "Journal of {F}unctional {P}rogramming",
  year =	 1997,
  volume =	 7,
  number =	 5,
  pages =	 "549--554"
}

@PhdThesis{  bove:lic,
  author = 	 "Ana Bove",
  title = 	 "Programming in {M}artin-{\"o}f {T}ype
		  {T}heory. {U}nification: {A} non-trivial {E}xample",
  school = 	 "{C}halmers {U}niversity of {T}echnology, {S}weden",
  year = 	 1999,
  type =	 "{L}icentiate {T}hesis"
}

@Article{robinson:unification,
  author = 	 "Alan Robinson",
  title = 	 "{A} {M}achine-oriented {L}ogic {B}ased on the
  {R}esolution {P}rinciple",
  journal =	 "{J}ournal of the {ACM}",
  year =	 1965,
  volume =	 12,
  pages =	 "23--41"
}

@TechReport{rouyer:unification,
  author = 	 "Joseph Rouyer",
  title = 	 " {D}{\'e}veloppement de l'algorithme
  d'unification dans le {C}alcul des {C}onstructions avecs types inductifs",
  institution =  "INRIA-Lorraine",
  year = 	 1992,
  number =	 1795,
  OPTmonth =	 nov
}

@PhdThesis{coen:unification,
  author = 	 "Martin Coen",
  title = 	 "{I}nteractive {P}rogram {D}erivation",
  school = 	 "{U}niversity of {C}ambridge",
  year = 	 1992
}

@InProceedings{jaume:unification,
  author = 	 "Mathieu Jaume",
  title = 	 "{U}nification : a {C}ase {S}tudy in
  {T}ransposition of {F}ormal {P}roperties",
  editor =	 "{E}lsa. {G}unter and {A}my {F}elty",
  booktitle =	 "{S}upplementary {P}roceedings of
                  the 10th {I}nternational {C}onference on {T}heorem {P}roving
                  in {H}igher {O}rder {L}ogics: {P}oster session {TPHOL}s'97",
  year =	 1997,
  pages =	 "79--93"
}

@Article{manna.waldinger:unification,
  author = 	 "Zohar Manna and Richard Waldinger",
  title = 	 "{D}eductive {S}ynthesis of the {U}nification {A}lgorithm",
  journal =	 "{S}cience of {C}omputer {P}rogramming",
  volume =	 1,
  pages =	 "5--48",
  year =	 1981,
  note =	 "{N}orth-{H}olland"
}

@Article{paulson:unification,
  author = 	 "Lawrence Paulson",
  title = 	 "{V}erifying the {U}nification {A}lgorithm in {LCF}",
  journal =	 "{S}cience of {C}omputer {P}rogramming",
  volume =	 5,
  pages =	 "143--169",
  year =	 1985,
  note =	 "{N}orth-{H}olland"
}

@InProceedings{backhouse.jansson.jeuring.meertens:generic,
  author = 	 "Roland Backhouse and Patrik Jansson and Johan
		  Jeuring and Lambert Meertens",
  title = 	 "Generic {P}rogramming---{A}n {I}ntroduction",
  crossref =	 "lncs1608",
  pages =	 "28--115"
}

@InCollection{dybjer:families,
  author = 	 "Peter Dybjer",
  title = 	 "Inductive {S}ets and {F}amilies in {M}artin-{L}{\"o}f's {T}ype
		  {T}heory",
  crossref =	 "huet.plotkin:logical.frameworks"
}

@InProceedings{  turner:strong.functional,
  author = 	 "David Turner",
  title = 	 "Elementary {S}trong {F}unctional {P}rogramming",
  crossref =	 "lncs1022"
}

@InProceedings{jansson.jeuring:polyp,
  author = 	 "Patrik Jansson and Johan Jeuring",
  title = 	 "Poly{P}---a polytypic programming language extension",
  crossref =	 "popl97",
  pages =	 "470--482"
}

@TechReport{      luo.pollack:legomanual,
  author        = "Zhaohui Luo and Robert Pollack",
  title         = "{LEGO} {P}roof {D}evelopment {S}ystem: {U}ser's {M}anual",
  institution   = lfcs,
  year          = 1992,
  number        = "ECS-LFCS-92-211",
  OPTmonth         = may
}

@InProceedings{mcadam:type.debugging,
  author =       {Bruce J. McAdam},
  title =        {Generalising Techniques for Type Explanation},
  booktitle =    {Scottish Functional Programming Workshop},
  year =         1999,
  pages = {243--252},
  note = {Heriot-Watt Department of Computing and Electrical Engineering Technical Report RM/99/9}
}

@Article{bird.paterson:debruijn.nested,
  author = 	 "Richard Bird and Ross Paterson",
  title = 	 "de {B}ruijn notation as a nested datatype",
  journal =	 "Journal of {F}unctional {P}rogramming",
  year =	 1999,
  volume =	 9,
  number =	 1,
  pages =	 "77-92"
}

@InProceedings{bird.meertens:nested,
  author = 	 "Richard Bird and Lambert Meertens",
  title = 	 "Nested {D}atatypes",
  crossref =	 "lncs1422",
  pages =	 "52--67"
}

@InProceedings{okasaki:square.matrices,
  author = 	 "Chris Okasaki",
  title = 	 "{F}rom {F}ast {E}xponentiation to {S}quare {M}atrices: {A}n
		  {A}dventure in {T}ypes",
  booktitle =	 icfp # " '99",
  year =	 1999
}

@InCollection{joyal:species,
  author = 	 "Andr\'{e} Joyal",
  title = 	 "Foncteurs analytiques et esp\`{e}ces de structures",
  booktitle =	 "Combinatoire \'{e}numerative",
  publisher =	 "Springer-Verlag",
  year =	 1987,
  volume =	 1234,
  series =	 "LNM",
  pages =	 "126--159"
}

@PhdThesis{mcbride:patternmatching,
  author = 	 "Fred McBride",
  title = 	 "Computer Aided Manipulation of Symbols",
  school = 	 "Queen's University of Belfast",
  year = 	 1970
}

@Proceedings{icfp98,
  title = 	 icfp # " '98",
  booktitle =	 icfp # " '98",
  year = 	 1998,
  OPTmonth =        sep,
  organization = "ACM"
}

@Proceedings{     lncs1608,
  title         = "Advanced {F}unctional {P}rogramming,
		   {T}hird {I}nternational {S}ummer {S}chool
                  ({AFP} '98); Braga, Portugal",
  booktitle         = "Advanced {F}unctional {P}rogramming,
		   {T}hird {I}nternational {S}ummer {S}chool
                  ({AFP} '98); {B}raga, {P}ortugal",
  year          = 1998,
  editor =	 "S. Doaitse Sweierstra and Pedro R. Henriques and
		  Jos{\'e} N. Oliveira",
  volume        = 1608,
  series        = lncs,
  publisher     = "Springer-Verlag",
}

@InProceedings{paulin:extraction,
  author = 	 {Christine Paulin-Mohring},
  title = 	 "{Extracting \protect{$F^\omega$} Programs from
                 Proofs in the Calculus of Constructions}",
  crossref =	 "popl89"
}

@Book{huet.plotkin:logical.frameworks,
  title = 	 "Logical {F}rameworks",
  booktitle = 	 "Logical {F}rameworks",
  publisher = 	 "CUP",
  year = 	 1991,
  editor =	 "G{\'e}rard Huet and Gordon Plotkin"
}

@Proceedings{lncs1837,
  title = 	 "Mathematics of {P}rogram {C}onstruction",
  booktitle = 	 "Mathematics of {P}rogram {C}onstruction",
  year = 	 2000,
  volume =	 1837,
  editor =	 "Roland Backhouse and Jos\'{e} Nuno Oliviera",
  series        = lncs,
  publisher     = "Springer-Verlag"
}

@Proceedings{lncs1782,
  booktitle = 	 "Proceedings of the 9th
                {E}uropean {S}ymposium on {P}rogramming, ESOP 2000",
  year = 	 2000,
  volume =	 1782,
  series =	 lncs,
  publisher =	 "Springer-Verlag",
  OPTmonth =	 "March"
}

@Proceedings{     lncs1022,
  booktitle = 	 "{F}unctional {P}rogramming {L}anguages in
		  {E}ducation, {F}irst {I}nternational {S}ymposium",
  year = 	 1995,
  volume =	 1022,
  series =	 lncs,
  publisher =	 "Springer-Verlag"
}

@Proceedings{lncs1422,
  title = 	 "{M}athematics of {P}rogram {C}onstruction",
  booktitle = 	 "{M}athematics of {P}rogram {C}onstruction",
  year = 	 1998,
  volume =	 1422,
  series =	 lncs,
  publisher =	 "Springer-Verlag"
}

@Proceedings{     lncs1512,
  title         = "Types for Proofs and Programs, '96",
  booktitle     = "Types for Proofs and Programs, '96",
  year          = 1998,
  editor =	 "E. Gim{\'e}nez and C. Paulin-Mohring",
  series        = lncs,
  volume        = 1512,
  publisher     = sv
}

@Proceedings{     lncs1158,
  title         = "Types for Proofs and Programs, '95",
  booktitle     = "Types for Proofs and Programs, '95",
  year          = 1995,
  series        = lncs,
  volume        = 1158,
  publisher     = sv
}

@Proceedings{     lncs996,
  title         = "{Types for Proofs and Programs, '94}",
  booktitle     = "{Types for Proofs and Programs, '94}",
  year          = 1994,
  editor =	 "Peter Dybjer and Bengt Nordstr{\"o}m and Jan Smith",
  series        = lncs,
  volume        = 996,
  publisher     = sv
}

@Proceedings{     lfworkshop90,
  title         = "Electronic {P}roceedings of the {F}irst {A}nnual {BRA} {W}orkshop on
                  {L}ogical {F}rameworks ({A}ntibes, {F}rance)",
  booktitle     = "{E}lectronic {P}roceedings of the {F}irst {A}nnual {BRA} {W}orkshop on
                  {L}ogical {F}rameworks ({A}ntibes, {F}rance)",
  editor        = "G{\'e}rard Huet and Gordon Plotkin",
  year          = 1990,
  note           = "Available in {\texttt{http://www.lfcs.informatics.ed.ac.uk/research/types-bra/proc/proc90.ps.gz}}"

}

@Proceedings{     lfworkshop92www,
  title         = "Electronic {P}roceedings of the {T}hird {A}nnual {BRA} {W}orkshop on
                  {L}ogical {F}rameworks ({B}{\aa}stad, {S}weden)",
  booktitle         = "Electronic {P}roceedings of the {T}hird {A}nnual {BRA} {W}orkshop on
                  {L}ogical {F}rameworks ({B}{\aa}stad, {S}weden)",
  editor        = "Bengt \protect{{Nordstr{\"o}m}} and Kent Petersson and Gordon Plotkin",
  year          = 1992,
  note           = "Available in {\texttt{http://www.lfcs.informatics.ed.ac.uk/research/types-bra/proc/proc92.ps.gz}}"

}

@Proceedings{     lfworkshop92,
  title         = "Electronic {P}roceedings of the {T}hird {A}nnual {BRA} {W}orkshop on
                  {L}ogical {F}rameworks ({B}{\aa}stad, {S}weden)",
  booktitle         = "Electronic {P}roceedings of the {T}hird {A}nnual {BRA} {W}orkshop on
                  {L}ogical {F}rameworks ({B}{\aa}stad, {S}weden)",
  editor        = "Bengt \protect{{Nordstr{\"o}m}} and Kent Petersson and Gordon Plotkin",
  year          = 1992
}

@proceedings{clmp:types00,
   title     = "Types for {P}roofs and {P}rograms ({P}roceedings of the
                {I}nternational {W}orkshop, {TYPES'00})"
  ,booktitle     = "Types for {P}roofs and {P}rograms ({P}roceedings of the
                {I}nternational {W}orkshop, {TYPES'00})"
  ,year      = "2002"
  ,editor    =  "Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack"
  ,publisher = "Springer-Verlag"
  ,series    = LNCS
  ,volume    = 2277

}

@Proceedings{lncs201,
  title =        {{F}unctional {P}rogramming {L}anguages and
                  {C}omputer {A}rchitecture},
  booktitle =        {{F}unctional {P}rogramming {L}anguages and
                  {C}omputer {A}rchitecture},
  year =         1985,
  editor =       {Jean-Pierre Jouannaud},
  volume =       201,
  series =       lncs,
  OPTmonth =        sep,
  publisher =    sv
}

@Proceedings{     lncs664,
  title         = "{Int. Conf. Typed Lambda Calculi and
                  Applications TLCA'93}",
  booktitle     = "{Int. Conf. Typed Lambda Calculi and
                  Applications TLCA'93}",
  year          = 1993,
  editor        = "Marc Bezem and Jan-Friso Groote",
  volume        = 664,
  series        = lncs,
  publisher     = sv
}

%%%

@InBook{Szabo:gentzenLJ,
  author =	 {Gerhard Gentzen},
  OPTeditor =	 {Manfred Szabo},
  title = 	 {Investigations into logical deduction},
  chapter = 	 {3 of~\protect{\cite{Szabo:gentzen}}},
  publisher = 	 {North-Holland},
  year = 	 1935
}

@Book{Szabo:gentzen,
  OPTauthor =	 {Manfred Szabo},
  editor =	 {Manfred Szabo},
  title = 	 {The collected papers of {Gerhard Gentzen}},
  publisher = 	 {North-Holland},
  year = 	 1969
}

@InProceedings{Herbelin:ljt,
  author = 	 {Hugo Herbelin},
  title = 	 {A \protect{\(\lambda\)}-calculus structure isomorphic to sequent calculus},
  booktitle = 	 {Proceedings of {CSL}'94},
  pages =	 {67--75},
  year =	 1995,
  volume =	 933,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{Dyckhoff:mj,
  author = 	 {Roy Dyckhoff and Luis Pinto},
  title = 	 {Cut-elimination and a permutation-free sequent calculus for intuitionistic logic},
  journal = 	 {Studia Logica},
  year = 	 {1998},
  OPTkey = 	 {},
  volume =	 {60},
  OPTnumber = 	 {},
  pages =	 {107--118},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@PhdThesis{Pym:thesis,
  author = 	 {David Pym},
  title = 	 {Proofs, Search and Computation in General Logic},
  school = 	 {University of Edinburgh},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  note =	 {Available as {CST-69-90}, also
 published as {ECS-LFCS-90-125}},
  OPTannote = 	 {}
}

@Misc{Wadler:sequent,
  OPTkey = 	 {},
  author =	 {Philip Wadler},
  title =	 {A {Curry-Howard} isomorphism for sequent calculus},
  howpublished = {Talk given at the \protect{\epsrc\ \logfit} {Final Workshop}, Fairbairn House, Leeds},
  OPTmonth = 	 {},
  year =	 {1994},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{nordstrom:programming,
  author =	 {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
  title = 	 {Programming in {Martin-L{\"o}f}'s type theory: an introduction},
  publisher = 	 {Oxford University Press},
  year = 	 1990
}

@Misc{Wadler:view-proposal,
  OPTkey = 	 {},
  author =	 {Warren Burton and Erik Meijer and Patrick Samson and Simon Thompson and Philip Wadler},
  title =	 {Views: {An} {Extension} to {Haskell} {Pattern} {Matching}},
  howpublished = {},
  OPTmonth = 	 {},
  year =	 {1996},
  note =	 {Available from \url{http://www.haskell.org/development/views.html}},
  OPTannote = 	 {}
}

@Misc{peytonjones:pattern-guards,
  OPTkey = 	 {},
  author =	 {Simon Peyton{~}Jones},
  title =	 {A new view of guards},
  howpublished = {},
  year =	 {1997},
  OPTmonth =         apr,
  note =	 {Available from \url{http://research.microsoft.com/Users/simonpj/Haskell/guards.html}},
  OPTannote = 	 {}
}

@Misc{peytonjones:pattern-guards-transformational,
  OPTkey = 	 {},
  author =	 {Simon Peyton{~}Jones and Martin Erwig},
  title =	 {Pattern guards and transformational patterns},
  howpublished = "{In Proceedings of the 2000 Haskell Workshop}",
  note   =       {Available from \url{http://research.microsoft.com/Users/simonpj/Haskell/pat.ps.gz}},
  year =	 {2000},
  OPTmonth =     {},
  OPTannote = 	 {}
}

@Misc{pollack:changes94,
  OPTkey = 	 {},
  author =	 {Robert Pollack},
  title =	 {{Incremental} {Changes} in {LEGO}:1994},
  OPThowpublished = {},
  OPTmonth = 	 {},
  year =	 {1994},
  note =	 {Available from \url{ftp://ftp.dcs.ed.ac.uk/pub/lego/changes94.ps.gz}},
  OPTannote = 	 {}
}

@PhdThesis{randy:thesis,
  author = 	 {Robert Pollack},
  title = 	 "{The Theory of LEGO}",
  school = 	 "{University of Edinburgh}",
  year = 	 {1995},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  note =	 {Available from \url{http://www.lfcs.informatics.ed.ac.uk/reports/95/ECS-LFCS-95-323/}},
  OPTannote = 	 {}
}

@Article{harper.pollack:universes,
  author = 	 {Robert Harper and Randy Pollack},
  title = 	 {Type Checking with Universes},
  journal = 	 tcs,
  year = 	 {1991},
  OPTkey = 	 {},
  volume =	 {89},
  OPTnumber = 	 {},
  pages =	 {107--136},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@INPROCEEDINGS{courant02tphols,
  AUTHOR = {Judica{\"e}l Courant},
  TITLE = {Explicit Universes for the Calculus of Constructions},
  CROSSREF = {tphols02},
  YEAR = 2002,
  PAGES = {115--130},
  TOPICS = {team},
  TYPE_PUBLI = {icolcomlec},
  URL = {http://www.lri.fr/~jcourant/papers/02/ExplUniv.ps.gz}
}

@InProceedings{paul.luo:lfinductive,
  author = 	 {Paul Callaghan and Zhaohui Luo},
  title = 	 {{Implementation} {Techniques} for {Inductive} {Types} in {Plastic}},
  booktitle = 	 {Proceedings {TYPES}'99},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {94--113},
  year =	 {2000},
  OPTeditor = 	 {},
  volume =	 {1956},
  OPTnumber = 	 {},
  series =	 lncs,
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 sv,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{altenkirch.mcbride:generic,
  author = 	 {Thorsten Altenkirch and Conor McBride},
  title = 	 "{Generic Programming within Dependently Typed Programming}",
  booktitle = 	 "{Proceedings of the {IFIP}~2.1 Working Conference on Generic Programming, 2002}",
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2002},
  editor =	 {Jeremy Gibbons and Johan Jeuring},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {Kluwer},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{xi.pfenning:array.bounds,
  author = 	 {Hongwei Xi and Frank Pfenning},
  title = 	 {Eliminating array bound checking through dependent types},
  booktitle = 	 "{Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98)}",
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {249--257},
  year =	 {1998},
  OPTeditor =	 {Keith D. Cooper},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {June},
  OPTorganization = {},
  publisher =	 {ACM Press},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InCollection{barendregt:lambdacalculi,
  author = 	 {Henk Barendregt},
  title = 	 "{Lambda Calculi with Types}",
  booktitle = 	 "{Handbook of Logic in Computer Science}",
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  publisher =	 {Oxford University Press},
  year =	 {1992},
  editor =	 {Samson Abramsky and Dov Gabbay and Tom Maibaum},
  volume =	 {II},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{barendregt:lambdacalculus,
  ALTauthor = 	 {Henk Barendregt},
  ALTeditor = 	 {},
  title = 	 "{The Lambda Calculus: Its Syntax and Semantics (revised edition)}",
  publisher = 	 {North Holland},
  year = 	 {1984},
  OPTkey = 	 {},
  volume =	 {103},
  OPTnumber = 	 {},
  series =	 {Studies in Logic and the Foundations of Mathematics},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@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
}

@Proceedings{     popl89,
  key           = "POPL'89",
  title         = "16th {A}nnual {S}ymposium on Principles of {P}rogramming {L}anguages
                  (POPL)",
  booktitle     = "Proceedings of {POPL} '89",
  organization  = "ACM",
  OPTmonth         = jan,
  year          = 1989,
  crossrefonly  = 1
}

@Proceedings{     popl97,
  key           = "POPL'97",
  title         = "24th {A}nnual {S}ymposium on Principles of {P}rogramming {L}anguages
                  (POPL) (Paris, France)",
  booktitle     = "Proceedings of {POPL} '97",
  organization  = "ACM",
  OPTmonth         = jan,
  year          = 1997,
  crossrefonly  = 1
}

@Proceedings{     fpca89,
  key           = "FPCA'89",
  title         = "{Functional Programming
                  and Computer Architecture}",
  booktitle     = "Proceedings of {FPCA} '89",
  organization  = "ACM",
  OPTmonth         = jan,
  year          = 1989,
  crossrefonly  = 1
}

@Proceedings{     lncs806,
  title         = "Types for Proofs and Programs",
  booktitle     = "Types for Proofs and Programs",
  editor        = "Henk Barendregt and Tobias Nipkow",
  note          = "{Selected papers from the Int. Workshop TYPES
                  '93, Nijmegen, May 1993}",
  publisher     = sv,
  series        = "LNCS 806",
  year          = 1994
}

@Proceedings{     lncs417,
  title         = "COLOG-88. International Conference on Computer Logic",
  booktitle     = "COLOG-88. International Conference on Computer Logic",
  editor        = "Per Martin-L{{\"o}f} and Grigori Mints",
  publisher     = sv,
  series        = lncs,
  volume        = 417,
  year          = 1990
}

@InProceedings{Kahl-Scheffczyk-2001,
  author =  {Wolfram Kahl and Jan Scheffczyk},
  title =  {Named Instances for Haskell Type Classes},
  crossref = {Haskell2001},
  note = {See also: \textsf{http://ist.unibw-muenchen.de/Haskell/NamedInstances/}},
  bibliographies = {RelMiCS}
}

@Proceedings{Haskell2001,
  title =  {Proc.\null{} Haskell Workshop 2001, Firenze},
  booktitle =  {Proc.\null{} Haskell Workshop 2001},
  year =  {2001},
  editor =  {Ralf Hinze},
  volume =  {59},
  number =  {2},
  series =  ENTCS,
}

@Proceedings{     popl82,
  title         = "Ninth "  # popl,
  booktitle     = "Ninth "  # popl # " (Albuquerque, NM)",
  organization  = "ACM",
  gisignatur    = "mat 12.1.1-55",
  month         = "January",
  year          = 1982,
  crossrefonly  = 1
}

@Proceedings{     lncs1258,
  title         = "10th International Workshop on Computer Science Logic (CSL
                  '96)",
  booktitle     = "Computer Science Logic (CSL '96)",
  publisher     = sv,
  series        = lncs,
  volume        = "1258",
  year          = 1997
}

@PROCEEDINGS{tphols02,
  TITLE = {Theorem Proving in Higher Order Logics:
                           15th International Conference, TPHOLs 2002},
  BOOKTITLE = {Theorem Proving in Higher Order Logics:
                           15th International Conference, TPHOLs 2002},
  EDITOR = {Victor A. {Carre\~{n}o} and C\'{e}sar A. {Mu\~{n}oz} and Sofi\`{e}ne Tahar},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 2410,
  YEAR = 2002,
  PUBLISHER = {{Sprin\-ger-Verlag}},
  MONTH = AUG,
  ADDRESS = {Hampton, VA, USA}
}

@proceedings{hw2004,
  Title = {Proceedings of the {ACM} {SIGPLAN} {H}askell {W}orkshop 2004,
           Snowbird, Utah},
  Booktitle={Proceedings of the {ACM} {SIGPLAN} {H}askell {W}orkshop 2004,
           Snowbird, Utah},
  publisher = {ACM},
  editor = {Henrik Nilsson},
  year={2004}
}

gha_language: Haskell


text:
file(REMOVE_RECURSE
  "CMakeFiles/fbow_test_cpu_x86.dir/test_cpu_x86.cpp.o"
  "fbow_test_cpu_x86"
  "fbow_test_cpu_x86.pdb"
)

# Per-language clean rules from dependency scanning.
foreach(lang CXX)
  include(CMakeFiles/fbow_test_cpu_x86.dir/cmake_clean_${lang}.cmake OPTIONAL)
endforeach()

license: MIT

repository: qiaozhijian/fbow-modify

license_type: permissive

repo_name: qiaozhijian/fbow-modify

branch_name: refs/heads/master

extension: cmake


text:
#
#  mafMacroInstallProject.cmake
#  maf
#
#  Created by Daniele Giunchi - Paolo Quadrani on 10/09/10.
#  Copyright 2011 SCS-B3C. All rights reserved.
#
#  See Licence at: http://tiny.cc/QXJ4D
#
#

MACRO(mafMacroInstallProject executable)
SET_TARGET_PROPERTIES( ${PROJECT_NAME} PROPERTIES OUTPUT_NAME "${PROJECT_NAME}" )

if(${executable})
  IF (APPLE)
    set(lib_ext "dylib")

    set(TARGET_LOC)
    set(DEST_ABSOLUTE_DIR)
    get_target_property(TARGET_LOC ${PROJECT_NAME} LOCATION)
    get_filename_component(DEST_ABSOLUTE_DIR ${TARGET_LOC} PATH)

    set(MACOS_BUNDLE_DIR "${DEST_ABSOLUTE_DIR}")
# DEBUG
    SET(SOURCE_DIR   "${LIBRARY_OUTPUT_PATH}/Debug")
    SET(TARGET_DIR   ${MACOS_BUNDLE_DIR})

    FILE(GLOB file_list ${SOURCE_DIR}/*.${lib_ext})
    foreach(filelib ${file_list})
      get_filename_component(fileName ${filelib} NAME)
      add_custom_command(TARGET ${PROJECT_NAME} POST_BUILD
                          COMMAND ${CMAKE_COMMAND} -E copy ${filelib} ${TARGET_DIR}/${fileName} )
    endforeach(filelib ${file_list})

    set(file_list)
#RELEASE
    SET(SOURCE_DIR   "${LIBRARY_OUTPUT_PATH}/Release")
    SET(TARGET_DIR   ${MACOS_BUNDLE_DIR})

    FILE(GLOB file_list ${SOURCE_DIR}/*.${lib_ext})
    foreach(filelib ${file_list})
      get_filename_component(fileName ${filelib} NAME)
      add_custom_command(TARGET ${PROJECT_NAME} POST_BUILD
                          COMMAND ${CMAKE_COMMAND} -E copy ${filelib} ${TARGET_DIR}/${fileName} )
    endforeach(filelib ${file_list})
    set(file_list)
#
    SET(SOURCE_DIR   "${LIBRARY_OUTPUT_PATH}")
    SET(TARGET_DIR   ${MACOS_BUNDLE_DIR})

    FILE(GLOB file_list ${SOURCE_DIR}/*.${lib_ext})
    foreach(filelib ${file_list})
      get_filename_component(fileName ${filelib} NAME)
      add_custom_command(TARGET ${PROJECT_NAME} POST_BUILD
                          COMMAND ${CMAKE_COMMAND} -E copy ${filelib} ${TARGET_DIR}/${fileName} )
    endforeach(filelib ${file_list})

  ENDIF (APPLE)
endif(${executable})

ENDMACRO()


text:
# \brief adds for the given target a fake executable targets which allows all
#        headers and symbols to be shown in IDEs.
# \param target_name Which target properties should be added to the IDE support target.
function(target_add_ide_support target_name)
  if (NOT TARGET ${target_name})
    message(FATAL_ERROR "No target defined with name ${target_name}, cannot target_add_ide_support it.")
  endif()

  set (target_for_ide "${target_name}_ide_support")
  if (NOT TARGET ${target_for_ide})
      file(GLOB_RECURSE target_for_ide_srcs "*.h" "*.hpp" "*.hxx" "*.c" "*.cpp" "*.cxx")
      add_executable(${target_for_ide} ${target_for_ide_srcs})
      set_target_properties(${target_for_ide} PROPERTIES EXCLUDE_FROM_ALL 1 EXCLUDE_FROM_DEFAULT_BUILD 1)
  endif()

  get_target_property(dirs ${target_name} INCLUDE_DIRECTORIES)
  target_include_directories(${target_for_ide} PRIVATE ${dirs})

endfunction(target_add_ide_support)

gha_license_id: MIT


text:
@article{Marcon2014a,
 abstract = {Traditional measures of diversity, namely the number of species as well as Simpson's and Shannon's indices, are particular cases of Tsallis entropy. Entropy decomposition, i.e. decomposing gamma entropy into alpha and beta components, has been previously derived in the literature. We propose a generalization of the additive decomposition of Shannon entropy applied to Tsallis entropy. We obtain a self-contained definition of beta entropy as the information gain brought by the knowledge of each community composition. We propose a correction of the estimation bias allowing to estimate alpha, beta and gamma entropy from the data and eventually convert them into true diversity. We advocate additive decomposition in complement of multiplicative partitioning to allow robust estimation of biodiversity.},
 author = {Marcon, Eric and Scotti, Ivan and Hérault, Bruno and Rossi, Vivien and Lang, Gabriel},
 doi = {10.1371/journal.pone.0090289},
 journal = {Plos One},
 number = {3},
 pages = {e90289},
 title = {Generalization of the Partitioning of Shannon Diversity},
 url = {http://journals.plos.org/plosone/article?id=10.1371/journal.pone.0090289},
 volume = {9},
 year = {2014}
}

repository: EricMarcon/Home-Page

repo_name: EricMarcon/Home-Page

gha_language: TeX

extension: bib


text:
DESCRIPTION = "GLib 1.2 is a deprecated libray to \
provide support for old glib 1.2 based applications"
SECTION = "libs"
PRIORITY = "optional"
LICENSE = "LGPL"
DEPENDS += "glib-1.2-native"
DEPENDS_virtclass-native = ""
PR = "r5"

LEAD_SONAME = "libglib-1.2.*"

FILESDIR = "${@os.path.dirname(bb.data.getVar('FILE',d,1))}/glib-1.2-${PV}"

EXTRA_OECONF = "--disable-debug"

SRC_URI = "ftp://ftp.gtk.org/pub/gtk/v1.2/glib-${PV}.tar.gz \
           file://glibconfig-sysdefs.h \
	   file://depcomp \
	   file://glib-reconf-fix;apply=yes \
           file://posix-conf-changes;apply=yes \
           file://glib-config-use-pkg-config;apply=yes \
	   file://gcc-3.4-pretty_function;apply=yes"

S = "${WORKDIR}/glib-${PV}"

inherit autotools pkgconfig binconfig gettext

acpaths = ""
do_configure_prepend () {
	install -m 0644 ${WORKDIR}/glibconfig-sysdefs.h .
	install -m 0644 ${WORKDIR}/depcomp .
	rm -f ltconfig acinclude.m4 libtool ltmain.sh
}

do_install_virtclass-native () {
        oe_libinstall -so libglib ${D}${libdir}
        oe_libinstall -so -C gmodule libgmodule ${D}${libdir}
        oe_libinstall -so -C gthread libgthread ${D}${libdir}
        autotools_do_install
        install -d ${D}${includedir}/glib-1.2
        install -m 0644 glibconfig.h glib.h ${D}${includedir}/glib-1.2/
        install -d ${D}${datadir}/aclocal
        install -m 0644 ${S}/glib.m4 ${D}${datadir}/aclocal/glib-1.2.m4
}

do_install_append () {
	install -d ${D}${includedir}/glib-1.2
	install -m 0644 glibconfig.h glib.h ${D}${includedir}/glib-1.2/
	install -d ${D}${datadir}/aclocal
	install -m 0644 ${S}/glib.m4 ${D}${datadir}/aclocal/glib-1.2.m4
}

FILES_${PN}-dev += "${libdir}/glib/include/glibconfig.h"

SRC_URI[md5sum] = "6fe30dad87c77b91b632def29dd69ef9"
SRC_URI[sha256sum] = "6e1ce7eedae713b11db82f11434d455d8a1379f783a79812cd2e05fc024a8d9f"

BBCLASSEXTEND = "native"

NATIVE_INSTALL_WORKS = "1"

repository: overo/overo-oe-natty

repo_name: overo/overo-oe-natty

branch_name: HEAD

extension: bb


text:
@import url("https://fonts.googleapis.com/css2?family=Special+Elite&display=swap");

.container {
  display: flex;
  flex-direction: column;
  align-items: center;
  padding-top: 70px;
  margin: 0 auto;
  max-width: 1400px;
}

.title {
  font-family: "Special Elite", cursive;
}

.title h1 {
  font-size: 4em;
}

.title p {
  font-size: 2em;
  text-align: center;
}

.logo {
  margin: 30px 0;
}

.conference,
.division,
.city {
  width: 400px;
  display: flex;
  justify-content: space-between;
  align-items: center;
}

.conference p,
.division p,
.city p {
  font-size: 1.7em;
  padding: 5px 0;
}

.conference span,
.division span,
.city span {
  font-weight: bold;
  font-size: 1.2em;
}

.history span {
  margin-left: 40px;
  display: inline-block;
}

.history span {
  margin-top: 20px;
  text-indent: 70px;
  font-size: 1.1em;
  line-height: 1.4;
}

extension: css


text:
DESCRIPTION = "NVIDIA TensorRT Prebuilt Plugins for deep learning"
LICENSE = "Proprietary"

inherit l4t_deb_pkgfeed features_check

HOMEPAGE = "http://developer.nvidia.com/tensorrt"

L4T_DEB_GROUP = "tensorrt"

SRC_COMMON_DEBS = "\
    libnvonnxparsers8_${PV}+cuda11.4_arm64.deb;downloadfilename=libnvonnxparsers8_${PV}+cuda11.4_arm64.deb;name=onnx;subdir=tensorrt \
    libnvonnxparsers-dev_${PV}+cuda11.4_arm64.deb;downloadfilename=libnvonnxparsers-dev_${PV}+cuda11.4_arm64.deb;name=onnxdev;subdir=tensorrt \
    libnvinfer-plugin8_${PV}+cuda11.4_arm64.deb;downloadfilename=libnvinfer-plugin8_${PV}+cuda11.4_arm64.deb;name=plugin;subdir=tensorrt \
    libnvinfer-plugin-dev_${PV}+cuda11.4_arm64.deb;downloadfilename=libnvinfer-plugin-dev_${PV}+cuda11.4_arm64.deb;name=plugindev;subdir=tensorrt \
"

ONNXSHA256SUM = "852be6ab118a215f59379e740f1f713bdcdf3d94437e44cc5fd816ab08009dc1"
ONNXDEVSHA256SUM = "5605ff4ad376e12e4e6728a17d86ad8cd898f71cbd56c096eb856e7795a15867"
PLUGINSHA256SUM = "a533e5d0c029be8ebfe67d4d4531ba08c8750373aeabc4bd6fb1f9abe8db92c1"
PLUGINDEVSHA256SUM = "63e70bdc9d31b76ee14dab39b26e60765a21217a7957fa23c508cda92e670bdb"

SRC_URI[onnx.sha256sum] = "${ONNXSHA256SUM}"
SRC_URI[onnxdev.sha256sum] = "${ONNXDEVSHA256SUM}"
SRC_URI[plugin.sha256sum] = "${PLUGINSHA256SUM}"
SRC_URI[plugindev.sha256sum] = "${PLUGINDEVSHA256SUM}"

COMPATIBLE_MACHINE = "(tegra)"

REQUIRED_DISTRO_FEATURES = "opengl"

LIC_FILES_CHKSUM = "file://usr/include/aarch64-linux-gnu/NvInferPlugin.h;endline=11;md5=ddd2b55ba0ff98b2a932ed025ffe3f25"

def extract_basever(d):
    ver = d.getVar('PV').split('-')[0]
    components = ver.split('.')
    return '%s.%s.%s' % (components[0], components[1], components[2])

def extract_majver(d):
    ver = d.getVar('PV').split('-')[0]
    return ver.split('.')[0]

BASEVER = "${@extract_basever(d)}"
MAJVER = "${@extract_majver(d)}"

S = "${WORKDIR}/tensorrt"

DEPENDS = "cuda-cudart cudnn tensorrt-core libcublas"

do_configure() {
    :
}

do_compile() {
    :
}

do_install() {
    install -d ${D}${includedir}
    install -m 0644 ${S}/usr/include/aarch64-linux-gnu/*.h ${D}${includedir}
    install -d ${D}${libdir}
    install -m 0644 ${S}/usr/lib/aarch64-linux-gnu/libnvinfer_plugin.so.${BASEVER} ${D}${libdir}
    install -m 0644 ${S}/usr/lib/aarch64-linux-gnu/libnvonnxparser.so.${BASEVER} ${D}${libdir}
    install -m 0644 ${S}/usr/lib/aarch64-linux-gnu/libnvinfer_plugin_static.a ${D}${libdir}
    install -m 0644 ${S}/usr/lib/aarch64-linux-gnu/libnvonnxparser_static.a ${D}${libdir}
    install -m 0644 ${S}/usr/lib/aarch64-linux-gnu/libonnx_proto.a ${D}${libdir}
    ln -s libnvinfer_plugin.so.${BASEVER} ${D}${libdir}/libnvinfer_plugin.so.${MAJVER}
    ln -s libnvinfer_plugin.so.${BASEVER} ${D}${libdir}/libnvinfer_plugin.so
    ln -s libnvonnxparser.so.${BASEVER} ${D}${libdir}/libnvonnxparser.so.${MAJVER}
    ln -s libnvonnxparser.so.${MAJVER} ${D}${libdir}/libnvonnxparser.so
}

PROVIDES = "tensorrt-plugins"
RPROVIDES:${PN} = "tensorrt-plugins"
RCONFLICTS:${PN} = "tensorrt-plugins"
RPROVIDES:${PN}-dev = "tensorrt-plugins-dev"
RCONFLICTS:${PN}-dev = "tensorrt-plugins-dev"

INHIBIT_PACKAGE_STRIP = "1"
INHIBIT_PACKAGE_DEBUG_SPLIT = "1"
INHIBIT_SYSROOT_STRIP = "1"

PACKAGE_ARCH = "${TEGRA_PKGARCH}"

repository: SOL-Space-Operating-Linux/meta-tegra

repo_name: SOL-Space-Operating-Linux/meta-tegra

gha_language: BitBake


text:
# Copyright (C) 2013, 2014 Freescale Semiconductor
# Released under the MIT license (see COPYING.MIT for the terms)

require gpu-viv-bin-mx6q.inc

SRC_URI[md5sum] = "8b9c4f6181acf46028e39508a970ecc1"
SRC_URI[sha256sum] = "7e5a3db22b99740756f408b881691f81c03090256754e44f69369bf039e9cbcf"

PACKAGE_FP_TYPE = "hardfp"

repository: MildePM/meta-jens

repo_name: MildePM/meta-jens


text:
@book{friedman2009elements,
  title = {The elements of statistical learning: Data Mining, Inference, and Prediction},
  author = {Friedman, Jerome and Hastie, Trevor and Tibshirani, Robert},
  year = {2009},
  edition = {2},
  publisher={Springer series in statistics Springer, Berlin}
}

@article{weatherwax2013solution,
  title = {A Solution Manual and Notes for: The Elements of Statistical Learning by Jerome Friedman, Trevor Hastie, and Robert Tibshirani},
  author = {Weatherwax, John L. and Epstein, David},
  url = "http://waxworksmath.com/Authors/G\_M/Hastie/hastie.html",
  year = {2013},
  month = {June}
}

@article{wu2016partial,
  title = {A Partial Solution Manual for: The Elements of Statistical Learning by Jerome Friedman, Trevor Hastie, and Robert Tibshirani},
  author = {Wenhao Wu},
  url = "https://github.com/huragok/IDA",
  year={2016}
}

@article{hastie1994flexible,
  title={Flexible discriminant analysis by optimal scoring},
  author={Hastie, Trevor and Tibshirani, Robert and Buja, Andreas},
  journal={Journal of the American statistical association},
  volume={89},
  number={428},
  pages={1255--1270},
  year={1994},
  publisher={Taylor \& Francis}
}

@article{baudat2000generalized,
  title={Generalized discriminant analysis using a kernel approach},
  author={Baudat, Gaston and Anouar, Fatiha},
  journal={Neural computation},
  volume={12},
  number={10},
  pages={2385--2404},
  year={2000},
  publisher={MIT Press}
}


text:
@inproceedings{zafeiriou2016facial,
 author = {Zafeiriou, S and Papaioannou, A and Kotsia, I and Nicolaou, M and Zhao, G},
 booktitle = {the-wild”: A survey and a new database,” in The IEEE Conference on Computer Vision and Pattern Recognition (CVPR) Workshops},
 title = {Facial affect},
 year = {2016}
}

repository: apapaion/academic-kickstart

repo_name: apapaion/academic-kickstart


text:
@book{chapman1990,
  title={The mathematical theory of non-uniform gases: an account of the kinetic theory of viscosity, thermal conduction and diffusion in gases},
  author={Chapman, Sydney and Cowling, Thomas George and Burnett, David},
  year={1990},
  publisher={Cambridge university press}
}
@book{batchelor2000,
  title={An introduction to fluid dynamics},
  author={Batchelor, Cx K and Batchelor, GK},
  year={2000},
  publisher={Cambridge university press}
}
@article{bezanson2017,
  title={Julia: A fresh approach to numerical computing},
  author={Bezanson, Jeff and Edelman, Alan and Karpinski, Stefan and Shah, Viral B},
  journal={SIAM review},
  volume={59},
  number={1},
  pages={65--98},
  year={2017},
  publisher={SIAM}
}
@inproceedings{jasak2007,
  title={OpenFOAM: A C++ library for complex physics simulations},
  author={Jasak, Hrvoje and Jemcov, Aleksandar and Tukovic, Zeljko and others},
  booktitle={International workshop on coupled methods in numerical dynamics},
  volume={1000},
  pages={1--20},
  year={2007},
  organization={IUC Dubrovnik Croatia}
}
@misc{clawpack2020,
  title={Clawpack software},
  author={{Clawpack Development Team}},
  url={http://www.clawpack.org},
  note={Version 5.7.1},
  doi={https://doi.org/10.5281/zenodo.4025432},
  year={2020}}
@article{Flux2018,
  author    = {Michael Innes and
               Elliot Saba and
               Keno Fischer and
               Dhairya Gandhi and
               Marco Concetto Rudilosso and
               Neethu Mariya Joy and
               Tejan Karmali and
               Avik Pal and
               Viral Shah},
  title     = {Fashionable Modelling with Flux},
  journal   = {CoRR},
  volume    = {abs/1811.01457},
  year      = {2018},
  url       = {https://arxiv.org/abs/1811.01457},
  archivePrefix = {arXiv},
  eprint    = {1811.01457},
  timestamp = {Thu, 22 Nov 2018 17:58:30 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1811-01457},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@misc{xiao2020,
  title={Using neural networks to accelerate the solution of the Boltzmann equation},
  author={Tianbai Xiao and Martin Frank},
  year={2020},
  eprint={2010.13649},
  archivePrefix={arXiv},
  primaryClass={physics.comp-ph}
}
@article{xiao2017,
  title={A well-balanced unified gas-kinetic scheme for multiscale flow transport under gravitational field},
  author={Xiao, Tianbai and Cai, Qingdong and Xu, Kun},
  journal={Journal of Computational Physics},
  volume={332},
  pages={475--491},
  year={2017},
  publisher={Elsevier}
}


text:
@article{MartinezDeceptionSenderReceiver2015,
 abstract = {Godfrey-Smith advocates for linking deception in sender-receiver games to the existence of undermining signals. I present games in which deceptive signals can be arbitrarily frequent, without this undermining information transfer between sender and receiver},
 author = {Martínez, Manolo},
 copyright = {All rights reserved},
 file = {/home/manolo/Zotero/storage/EMEQACY4/Martínez_2015_Deception in Sender–Receiver Games.pdf},
 journal = {Erkenntnis},
 number = {1},
 pages = {215--227},
 title = {Deception in Sender–Receiver Games},
 volume = {80},
 year = {2015}
}

repository: manolomartinez/my-website

repo_name: manolomartinez/my-website


text:
require libdrm.inc

SRC_URI = "git://anongit.freedesktop.org/git/mesa/drm"

S = "${WORKDIR}/git"

DEFAULT_PREFERENCE = "-1"

SRCREV = "97be70b45eccc37e98a1cecf360593f36956ea42"
PV = "2.4.61+git${SRCPV}"
PR = "${INC_PR}.0"

repository: rzr/meta-raspberrypi

repo_name: rzr/meta-raspberrypi

gha_language: C