CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory

CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. Barras, B., Jouannaud, J., Strub, P., & Wang, Q. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 143–151, 2011. IEEE Computer Society.

Paper doi bibtex

@inproceedings{DBLP:conf/lics/BarrasJSW11,
  author = {Bruno Barras and Jean{-}Pierre Jouannaud and
Pierre{-}Yves Strub and Qian Wang},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl = {https://dblp.org/rec/conf/lics/BarrasJSW11.bib},
  booktitle = {Proceedings of the 26th Annual {IEEE} Symposium on
Logic in Computer Science, {LICS} 2011, June 21-24,
2011, Toronto, Ontario, Canada},
  doi = {10.1109/LICS.2011.37},
  isbn = {978-0-7695-4412-0},
  pages = {143--151},
  publisher = {{IEEE} Computer Society},
  timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
  title = {CoQMTU: {A} Higher-Order Type Theory with a
Predicative Hierarchy of Universes Parametrized by a
Decidable First-Order Theory},
  url = {https://doi.org/10.1109/LICS.2011.37},
  year = {2011}
}

Downloads: 0