K is a semantical framework for formally describing the semantics of programming languages. It is also an environment that offers various tools to help programming with the languages specified in the formalism. It is for example possible to execute programs and to check some properties on them, using the KProver tool.

Dedukti is a logical framework allowing the interoperability of proofs between different formal proof tools. It is based on the lambda-calculus modulo theory, an extension of the type theory by adding rewriting rules in the conversion relation. The flexibility of this logical framework allows to encode many theories like 1st order logic or simple type theory.

Thanks to the logical framework Dedukti, the objective describes in this poster is to verify formal proofs about the semantics of programming languages, described in the semantical framework K, and to reuse of such proofs in different proof tools.

Working group : LVP