| Definitions by rewriting in the Calculus of Constructions F Blanqui Mathematical structures in computer science 15 (1), 37-92, 2005 | 124 | 2005 |
| Inductive-data-type systems F Blanqui, JP Jouannaud, M Okada Theoretical computer science 272 (1-2), 41-68, 2002 | 111 | 2002 |
| The calculus of algebraic constructions F Blanqui, JP Jouannaud, M Okada International Conference on Rewriting Techniques and Applications, 301-316, 1999 | 85 | 1999 |
| CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates F Blanqui, A Koprowski Mathematical Structures in Computer Science 21 (4), 827-859, 2011 | 83 | 2011 |
| A type-based termination criterion for dependently-typed higher-order rewrite systems F Blanqui International Conference on Rewriting Techniques and Applications, 24-39, 2004 | 69 | 2004 |
| Termination and confluence of higher-order rewrite systems F Blanqui International Conference on Rewriting Techniques and Applications, 47-61, 2000 | 69 | 2000 |
| CoLoR: a Coq Library on Rewriting and termination F Blanqui, S Coupet-Grimal, W Delobel, S Hinderer, A Koprowski Eighth International Workshop on Termination-WST 2006, 2006 | 66 | 2006 |
| The computability path ordering: The end of a quest F Blanqui, JP Jouannaud, A Rubio Computer Science Logic: 22nd International Workshop, CSL 2008, 17th Annual …, 2008 | 57 | 2008 |
| Static dependency pair method based on strong computability for higher-order rewrite systems K Kusakari, Y Isogai, M Sakai, F Blanqui IEICE TRANSACTIONS on Information and Systems 92 (10), 2007-2015, 2009 | 41 | 2009 |
| Higher-order dependency pairs F Blanqui arXiv preprint arXiv:1804.08855, 2018 | 37 | 2018 |
| Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems F Blanqui, C Riba LPAR 6, 105-119, 2006 | 34 | 2006 |
| Théorie des types et réécriture F Blanqui Université Paris Sud-Paris XI, 2001 | 34 | 2001 |
| Some axioms for mathematics F Blanqui, G Dowek, É Grienenberger, G Hondet, F Thiré FSCD 2021-6th International Conference on Formal Structures for Computation …, 2021 | 32 | 2021 |
| Inductive types in the calculus of algebraic constructions F Blanqui Fundamenta Informaticae 65 (1-2), 61-86, 2005 | 30 | 2005 |
| The computability path ordering F Blanqui, JP Jouannaud, A Rubio Logical methods in computer science 11, 2015 | 29 | 2015 |
| Decidability of type-checking in the Calculus of Algebraic Constructions with size annotations F Blanqui International Workshop on Computer Science Logic, 135-150, 2005 | 29 | 2005 |
| The new rewriting engine of dedukti G Hondet, F Blanqui arXiv preprint arXiv:2010.16115, 2020 | 25 | 2020 |
| Termination of rewrite relations on λ-terms based on Girard's notion of reducibility F Blanqui Theoretical computer science 611, 50-86, 2016 | 25 | 2016 |
| Argument filterings and usable rules in higher-order rewrite systems S Suzuki, K Kusakari, F Blanqui IPSJ Online Transactions 4, 114-125, 2011 | 25 | 2011 |
| Building decision procedures in the calculus of inductive constructions F Blanqui, JP Jouannaud, PY Strub Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual …, 2007 | 24 | 2007 |
Jean-Pierre JouannaudLSV, École Normale Supérieure de Paris-Saclay在 lix.polytechnique.fr 的电子邮件经过验证
