Paper: CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory (at LICS 2011)

Authors: Bruno Barras Jean-Pierre Jouannaud Pierre-Yves Strub Qian Wang

Abstract

No Abstract Available

BibTeX

  @InProceedings{BarrasJouannaudStru-CoQMTUAHigherOrderT,
    author = 	 {Bruno Barras and Jean-Pierre Jouannaud and Pierre-Yves Strub and Qian Wang},
    title = 	 {CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory},
    booktitle =  {Proceedings of the Twenty-Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 2011)},
    year =	 {2011},
    month =	 {June}, 
    pages =      {143--151},
    location =   {Toronto, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }