Pierre-yves Strub (史都伯)
Postdoc at
Tsinghua University
- LIAMA
- Beijing.
INRIA - FORMES project
Previously, Ph.D. student under the supervision of
Jean-Pierre Jouanaud.
TypiCal (ex. LogiCal) team
- INRIA Saclay - Ile de France
- Laboratoire d'Informatique de l'X
Office:
Offices 3-604, FIT Building, Tsinghua University
Haidian District, Beijing, 100084, CHINA
EMail: pierre-yves [at] strub.nu
Research
Software
- Coq Modulo Theories is an extension of the Coq proof assistant embedding, in its computational mechanism, validity entailment for user-defined first-order equational theories.
Publications
-
Coq Modulo Theory
19th EACSL Annual Conference on Computer Science and Logic - CSL 2010 -
Coq Modulo Theory - Short Paper
- with: Qian Wang
Short Presentation - 25th Logic In Computer Science - LICS 2010 -
Type Theory and Decision Procedures
Ph.D. Thesis -
From Formal Proofs to Mathematical Proofs: A safe, incremental way for building in first-order decision procedures
- [bib]
5th IFIP International Conference on Theoretical Computer Science
-
Building Decision Procedures in the Calculus of Inductive Constructions
- [bib]
16th EACSL Annual Conference on Computer Science and Logic - CSL 2007