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:
30 May - 10 June 2023: visit of Akihisa Yamada and Makoto Hamana by Frédéric Blanqui
Akihisa Yamada, Jérémy Dubut and Frédéric Blanqui updated isabelle_dedukti so that it works with the most recent version of Isabelle.
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.
