 |
王前(Qian WANG)Ph.D Student Tsinghua University, Main Building, room 11-301 Haidian District, Beijing 100084, P.R. China qw04ster@gmail.com |
Education.
- Currecntly, I am a joint Ph.D student of Tsinghua University (China) and Ecole Polytechnique (France).
- I got my bachelor degree of Engneering from Tsinghua University in 2008.
Research interests.
- Theory : The fundamental type theory of theorem prover Coq.
- Verification : Apply Coq in verifying hardware circuits, mathematics, software systems.
Publications.
| [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] |
Links.
