3月20日，應計算機科學國家重點實驗室邀請，法國格勒諾布爾綜合理工學院Jean-Francois Monin教授到軟件所進行訪問，并作題為Handcrafted Coq Inversions Made Operational on Operational Semantics的學術講座，講座由 Jean-Jacque Levy研究員主持。 

報告中，Jean-Francois Monin教授闡述了一種使用Coq工具在做定理證明時會用到的策略， 由于該技術可以降低證明過程的難度，使用范圍較廣。但問題是使用該技術后證明過程比較繁瑣，而且可控性差。針對該問題，他們提出了一種基于非斷言的歸納數據結構和反對角參數相結合的證明技術，不僅極大的縮減了證明過程，而且魯棒性更強。

Jean-Francois Monin教授的報告激起了與會人員的濃厚興趣，大家對該新的策略技術的適用范圍和應用前景十分關注。報告結束后，與會人員同Jean-Francois Monin教授進行了深入廣泛交流。

Jean-Francois Monin現任法國格勒諾布爾綜合理工學院(Universite de Grenoble )/約瑟夫傅利葉(Joseph Fourier)大學教授。他曾任法國國家科學研究中心(CNRS)、中法信息自動化與應用數學聯合實驗室(LIAMA) 研究員，并曾在法國電信研發部門工作，領導一個致力于形式化方法的研究團隊。2009年，擔任法國國家科學研究中心研究員，并在中法信息自動化與應用數學聯合實驗室(LIAMA) 從事科研工作。他的研究領域主要包括Coq的理論型證明等，這些證明輔助實現了分布式算法的設計、安全問題的解決和嵌入式軟件的實現等各項應用。

Jean-Francois Monin教授作報告