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
Activities:
6 December 2023: meeting in AIST with Akihisa Yamada, Frédéric Blanqui and Reynald Affeldt: discussion on the translation of Isabelle to Coq
1 December 2023: project meeting in AIST with Akihisa Yamada, Frédéric Blanqui, Makoto Hamana and Koko Muroya:
Frédéric gave a general introduction to proof system interoperability [slides]
Akihisa Yamada explained problems encountered with the translation of Isabelle proofs to Dedukti
Discussion of the new format proposal for term rewriting systems in the confluence and termination competitions
Makoto Hamana presented his work on Verifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
Koko presented some ongoing work on the use of rewriting techniques in functional programming compilation and evaluation, introduction to term evaluation and refinement systems
29 November - 7 December 2023: visit of Akihisa Yamada by Frédéric Blanqui to work on isabelle_dedukti and the translation of Isabelle proofs to Coq
13-15 November 2023: visit of Frédéric Blanqui by Akihisa Yamada, work on updating isabelle_dedukti to Isabelle 2023 and trying to handle AFP sessions
15-26 November 2022: visit of Akihisa Yamada and Makoto Hamana by Thiago Felicissimo
At AIST, Thiago presented his work on how to encode type systems in Dedukti so that conservativity is easy to prove, and how to translate the proofs from an impredicative system to a predicative one.
Thiago and Makoto discussed different approaches for proving the confluence and termination of higher-order rewrite systems.
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.
