K <> ML Formalization - Githubissues

Baltoli commented 1 year ago

Ongoing project to formalise AML (applicative matching logic) in Coq
We want to join the gap between this project and K
We'd like to be able to prove the simplification lemmas in the standard library; this would give us a way to do so - supports the current K workflow which is good at reachability claims already (e.g. lemmas)
Existing prototype translates KORE into AML; some of this is Python and some of this is on paper
Ideal outcome is: K definition -> AML theory -> coq -> re-export to K-compatible format
@h0nzZik would like to understand how we translate code to SMT queries

Initial discussion on Slack

Baltoli commented 1 year ago

@h0nzZik I have removed this from the K board for now as I'm not sure there's an actionable plan for the K team, but if you have questions or want to better understand why K does something please write it down here and let us know how we can help you!

fiedlr commented 1 year ago

Just wanted to say, thanks, guys!!! This will be a huge step forward! @Baltoli @h0nzZik

runtimeverification / k

K <> ML Formalization #3519