The B-Book: Assigning Programs to Meanings, 2005. ,
Towards Certified Meta-Programming with Typed Template-Coq, Interactive Theorem Proving -9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC, vol.10895, pp.20-39, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01809681
The operational package, 2010. ,
Specification and verification: the Spec# experience, Commun. ACM, vol.54, pp.81-91, 2011. ,
Programming with Algebraic Effects and Handlers, Journal of Logical and Algebraic Methods in Programming, vol.84, pp.108-123, 2015. ,
Resource-dependent algebraic effects, International Symposium on Trends in Functional Programming, pp.18-33, 2014. ,
Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011. ,
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification, Proceedings of the ACM on Programming Languages, vol.1, p.24, 2017. ,
Verifying effectful Haskell programs in Coq, Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, pp.125-138, 2019. ,
Mechanical Verification of Interactive Programs Specified by Use Cases, Proceedings of the Third FME Workshop on Formal Methods in Software Engineering, pp.61-67, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01255107
Programming-in-the-Large Versus Programming-in-the-Small, IEEE Trans. Software Eng, vol.2, issue.2, pp.80-86, 1976. ,
One Monad to Prove Them All, Programming Journal, vol.3, 2019. ,
Why3 -Where Programs Meet Provers, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, vol.7792, pp.125-128, 2013. ,
, PLDI 2002: Extended static checking for Java. SIGPLAN Notices, vol.48, pp.22-33, 2013.
Web Attack Detection Using ID3, Toward Category-Level Object Recognition, vol.4170, pp.323-332, 2006. ,
On Folk Theorems, Commun. ACM, vol.23, pp.379-389, 1980. ,
, 2015. Mathematics of Program Construction -12th International Conference, MPC 2015, vol.9129, 2015.
The Coq Proof Assistant ,
Mtac2: typed tactics for backward reasoning in Coq, ICFP, vol.2, p.31, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01890511
Freer Monads, More Extensible Effects, In ACM SIGPLAN Notices, vol.50, pp.94-105, 2015. ,
,
, From C to interaction trees: specifying, verifying, and testing a networked server, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019.
, , pp.234-248
Accessible Software Verification with Dafny, IEEE Software, vol.34, pp.94-97, 2017. ,
Modular Verification of Programs with Effects and Effects Handlers in Coq, 22st International Symposium on Formal Methods (FM 2018), 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01799712
Extraction in Coq: An Overview, Logic and Theory of Algorithms, 4th Conference on Computability in Europe, vol.5028, pp.359-369, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00338973
A Behavioral Notion of Subtyping, ACM Trans. Program. Lang. Syst, vol.16, pp.1811-1841, 1994. ,
Dijkstra monads for all, ICFP, vol.3, pp.1-104, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02398919
Applying "Design by Contract, IEEE Computer, vol.25, pp.40-51, 1992. ,
Ynot: Dependent Types for Imperative Programs, ACM Sigplan Notices, vol.43, pp.229-240, 2008. ,
A Technique for Software Module Specification with Examples (Reprint), Commun. ACM, vol.26, pp.75-78, 1983. ,
, FoCaLiZe: inside an F-IDE, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01203501
Un environnement pour la programmation avec types dépendants, 2008. ,
Proceedings (Lecture Notes in Computer Science), Otmane Aït Mohamed, Theorem Proving in Higher Order Logics, 21st International Conference, vol.5170, pp.278-293, 2008. ,
A predicate transformer semantics for effects (functional pearl), PACMPL, vol.3, 2019. ,
, Topics in Theoretical Computer Science -Second IFIP WG 1.8 International Conference, vol.10608, pp.91-105, 2017.
Interaction Trees: Representing Recursive and Impure Programs in Coq, The 47th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '20, 2013. ,
Mtac: a monad for typed tactic programming in Coq, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, pp.87-100, 2013. ,