Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions Y Bertot, P Castéran Springer Science & Business Media, 2013 | 3128 | 2013 |
Interactive theorem proving and program development. Texts in Theoretical Computer Science Y Bertot, P Castéran An EATCS Series, SpringerVerlag, 16, 2004 | 80 | 2004 |
Coq’Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science Y Bertot, P Castéran Springer, 2004 | 40 | 2004 |
Tasks, types and tactics for local computation systems P Castéran, V Filou Studia Informatica Universalis 9 (1), 39-86, 2011 | 32 | 2011 |
Interactive Theorem Proving and Program Development Y Bertod, P Castéran Springer, 2004 | 29 | 2004 |
A tutorial on [co-] inductive types in Coq E Giménez, P Castéran Technical report, INRIA, 1998 | 27 | 1998 |
Certifying distributed algorithms by embedding local computation systems in the coq proof assistant P Castéran, V Filou, M Mosbah Symbolic Computation in Software Science (SCSS 2009), To appear, 2009 | 24 | 2009 |
Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions. P Castéran, Y Bertot Springer Verlag, 2004 | 21 | 2004 |
A gentle introduction to type classes and relations in Coq P Castéran, M Sozeau Technical Report hal-00702455, version 1, 2012 | 19 | 2012 |
Reasoning about parametrized automata P Castéran, D Rouillard Proceedings, 8-th International Conference on Real-Time System 8, 107-119, 2000 | 10 | 2000 |
The negligible and yet subtle cost of pattern matching B Accattoli, B Barras Asian Symposium on Programming Languages and Systems, 426-447, 2017 | 8 | 2017 |
On addition schemes S Brlek, P Castéran, R Strandh TAPSOFT'91: Proceedings of the International Joint Conference on Theory and …, 1991 | 8 | 1991 |
Adaptive software based on correct-by-construction metamodels F Barbier, P Castéran, E Cariou, O Le Goaer Progressions and Innovations in Model-Driven Software Engineering, 308-325, 2013 | 7 | 2013 |
Utilisation en Coq de l’opérateur de description P Castéran Actes des Journées Francophones des Langages Applicatifs, 30-44, 2007 | 7 | 2007 |
On-line evaluation of powers using Euclid's algorithm S Brlek, P Castéran, L Habsieger, R Mallette RAIRO-Theoretical Informatics and Applications 29 (5), 431-450, 1995 | 7 | 1995 |
Le coq’art (v8) Y Bertot, P Castéran Online http://wwwsop. inria. fr/members/Yves. Bertot/coqartF. pdf, 2015 | 6 | 2015 |
* Proof by Reflection Y Bertot, P Castéran, Y Bertot, P Castéran Interactive Theorem Proving and Program Development: Coq’Art: The Calculus …, 2004 | 6 | 2004 |
Formal proofs of local computation systems P Castéran, V Filou, M Mosbah | 5 | 2009 |
On the importance of explicit domain modelling in refinement-based modelling design. Experiments with Event-B Y Aït-Ameur, I Ait-Sadoune, P Castéran, P Gibson, K Hacid, S Kherroubi, ... Abstract State Machines, Alloy, B, TLA, VDM, and Z: 6th International …, 2018 | 4 | 2018 |
Proof automation for type-logical grammars H Anoun, P Castéran, R Moot Rapport technique, Notes pour le cours d’ESSLLI, Nancy, 2004 | 4 | 2004 |