France-Japan Sakura 2022-2023 project

Participants: France: Frédéric Blanqui (French PI) Gilles Dowek Jean-Pierre Jouannaud Thiago Felicissimo (PhD student) Yoan Géran (PhD student) Gabriel Hondet (PhD student) Louise Dubois de Prisque (PhD student) Japan: Makoto Hamana (Japanese PI) Keisuke Nakano Kazuyuki Asada Kentaro Kikuchi Akihisa Yamada Jérémy Dubut Kazuhiko Sakaguchi (PhD student)

Scientific objective: As information systems have become one of the important social infrastructures, the security assurance of software has become a major issue. However, computer software is very difficult to construct and to guarantee its security. In order to provide a high level of reliability assurance for software in general, rather than for each individual problem, it is necessary to have software technology that is widely applicable and based on rigorous theory. The purpose of this project is to develop and apply an automatic theorem proving system for safety assurance technology for software, and to realize the advancement of software safety assurance technology. In order to achieve this goal, we aim to develop a theorem proving system as a basic theory to realize a highly functional theorem proving system. Specifically, the following topics will be studied:

• Integration of the Dedukti system by Blanqui (French delegate) and the SOL system by Hamana (Japanese delegate)
• Integration of higher-order rewriting theory and type theory to realize a theorem proving support system
• Introducing rewriting technology into functional programming languages, the theorem proving system Isabelle/HOL, and the Coq system to automatically prove the properties of confluence and termination
• Establish software verification techniques using these systems

News:

• 15-26 November 2022: visit of Akihisa Yamada and Makoto Hamana by Thiago Felicissimo

• July 2022: visit of Deducteam by Kazuhiko Sakaguchi
  • Kazuhiko Sakaguchi and Gabriel Hondet discussed the use of unification hints, canonical structures and type classes in the formalization of algebraic structures
  • Gabriel Hondet wrote some example of unification hints in Lambdapi
  • Talk of Kazuhiko Sakaguchi on Reflexive tactics for algebra, revisited
  • Talk of Kazuhiko Sakaguchi on Stability of mergesort, almost for free
  • Talk of Thiago Felicissimo on Adequate and Computational Encodings in the Logical Framework Dedukti
• 23 May - 6 June 2022: visit of Akihisa Yamada and Makoto Hamana by Frédéric Blanqui
  • Frédéric Blanqui, Akihisa Yamada and Jérémy Dubut worked on improving isabelle_dedukti, the export of Isabelle proofs to Dedukti and Lambdapi.
  • Frédéric Blanqui and Makoto Hamana reviewed in details the correctness proof of the General Schema in case of higher-order polymorphic types. Frédéric Blanqui rewrote the code exporting Lambdapi to the HRS and XTC proof formats.
  • Talk of Frédéric Blanqui at Gunma University on Introduction to proof system interoperability, the Dedukti language and the Lambdapi tool.