Research interests.


[1] Barras, B., Jouannaud, J. P., Strub, P. Y., & Wang, Q. (2011, June). CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on (pp. 143-151). IEEE. [PDF]
[2] Wang, Q., Barras, B.: Semantics of Intensional Type Theory extended with Decidable Equational Theories. In Rocca, S.R.D., ed.: Computer Science Logic 2013 (CSL2013). Volume 23 of Leibniz International Proceedings in Informatics (LIPIcs).,Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2013) 653?67 [PDF]
[3] Wang, Q. Functional Veri cation of High Performance Adders in Coq (Manualscript). [PDF]