HOAS -- bib entries

@inproceedings{Hof99,
  author       = {Martin Hofmann},
  title        = {Semantical Analysis of Higher-Order Abstract Syntax},
  booktitle    = {14th Symposium on Logic in Computer Science},
  organization = {LICS},
  month        = {July},
  year         = 1999,
  pages        = 204,
  url          = {citeseer.nj.nec.com/239229.html}
}

@inproceedings{PE88,
    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)},
    comment   = {journal = "SIGPLAN Notices", volume = "23", number = "7",},
    address   = {Atlanta, Georgia},
    publisher = {ACM Press},
    pages     = {199--208},
    month     = {June},
    year      = 1988
}

@inproceedings{DPS97,
  author    = {Jo{\"e}lle Despeyroux and Frank Pfenning and Carsten Sch{\"u}rmann},
  title     = {Primitive Recursion for Higher-Order Abstract Syntax},
  booktitle = {proc. of the {TLCA}'97 Int. Conference},
  publisher = {Springer-Verlag LNCS 1210},
  editor    = {Philippe de Groote and J. Roger Hindley},
  note      = {An extended version is available as CMU Technical Report CMU-CS-96-172},
  pages     = {147--163},
  year      = 1997,
  month     = {April}
}

@techreport{DPS96,
   author      = {Jo{\"e}lle Despeyroux and Frank Pfenning and Carsten Sch{\"u}rmann},
   title       = {Primitive Recursion for Higher-Order Abstract Syntax},
   institution = {Carnegie Mellon University},
   address     = {Pittsburgh, Pennsylvania},
   number      = {CMU-CS-96-172},
   month       = {August},
   year        = {1996}
}

@inproceedings{DFH95,
   author    = {Jo{\"e}lle Despeyroux and Amy Felty and Andr{\'e} Hirschowitz},
   title     = {Higher-Order Abstract Syntax in Coq},
   booktitle = {proceedings of the {TLCA} 95 Int. Conference on Typed Lambda Calculi and Applications},
   location  = {Edinburgh},
   editor    = {M. Dezani and G. Plotkin},
   publisher = {Springer-Verlag LNCS},
   volume    = {902},
   year      = {1995},
   month     = {April},
   pages     = {124--138}
}

@inproceedings{DL99a,
  author    = {Jo{\"e}lle Despeyroux and Pierre Leleu},
  title     = {Primitive recursion for higher-order abstract syntax with dependant types},
  booktitle = {Informal proceedings of the {FLoC}'99 {IMLA} Workshop on Intuitionistic Modal Logics and Applications},
  location  = {trento, Italy},
  month     = {June},
  year      = 1999
}

@inproceedings{DL99,
  author    = {Jo{\"e}lle Despeyroux and Pierre Leleu},
  title     = {A Modal Lambda-Calculus with Iteration and Case Constructs},
  booktitle = {Proc. of the annual Types seminar},
  location  = {Kloster Irsee, Germany},
  month     = {March},
  year      = 1999
}

@inproceedings{Sch01,
  author    = {Carsten Sch{\"u}rmann},
  title     = {Recursion for Higher-Order Encodings},
  booktitle = {Proceedings of Computer Science Logic (CSL 2001)},
  location  = {Paris, France},
  pages     = {585--599},
  year      = 2001
}

@unpublished{Sch01a,
  author  = {Carsten Sch{\"u}rmann},
  title   = {A Type-Theoretic Approach to Induction with Higher-Order Encodings},
  comment = {submitted.  on his web page, it appears with this title: Induction Principles for Higher-Order Abstract Syntax},
  year    = 2001
}

@incollection{DP96,
  author    = {Rowan Davies and Frank Pfenning},
  title     = {A Modal Analysis of Staged Computation},
  booktitle = {Conf. Record 23rd ACM SIGPLAN/SIGACT Symp. on Principles of Programming Languages, POPL'96},
  publisher = {ACM Press},
  address   = {New York},
  location  = {St. Petersburg Beach, FL, USA},
  pages     = {258--270},
  year      = 1996,
  url       = {citeseer.nj.nec.com/article/davies96modal.html}
}

@inproceedings{FM95,
  author    = {Furio Honsell and Marino Miculan},
  title     = {A Natural Deduction Approach to Dynamic Logics},
  booktitle = {Proceedings of TYPES'95},
  volume    = 1158,
  series    = {Lecture Notes in Computer Science},
  year      = 1995,
  pages     = {165--182},
  month     = {june},
  note      = {workshop on proofs and types}
}

@inproceedings{BA02,
  author    = {Eli Barzilay and Stuart Allen},
  title     = {Reflecting Higher-Order Abstract Syntax in {N}uprl},
  booktitle = {Theorem Proving in Higher Order Logics; Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Hampton, VA, August 2002},
  year      = 2002,
  editor    = {Victor A. Carre{\~n}o and C{\'e}zar A. Mu{\~n}oz and Sophi{\`e}ne Tahar},
  pages     = {23--32},
  publisher = {National Aeronautics and Space Administration},
}