Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

K <> ML Formalization #3519

Open
Baltoli opened this issue Jul 13, 2023 · 2 comments
Open

K <> ML Formalization #3519

Baltoli opened this issue Jul 13, 2023 · 2 comments

Comments

@Baltoli
Copy link
Contributor

Baltoli commented Jul 13, 2023 •
edited
Loading

  • 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
Copy link
Contributor Author

Baltoli commented Jul 13, 2023

@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
Copy link
Contributor

fiedlr commented Jul 13, 2023 •
edited
Loading

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

Baltoli pushed a commit that referenced this issue Nov 1, 2023
@rv-jenkins @tothtamas28 @radumereuta
Update dependency: haskell-backend/src/main/native/haskell-backend (#…
f48fb65 
…3187)

* haskell-backend/src/main/native/haskell-backend: 2c1ff15bd - Export z3 overlay alone in flake (#3519)

* Sync flake inputs to submodules

* haskell-backend/src/main/native/haskell-backend: 93a705112 - [#3493] Add total attribute (#3505)

* Sync flake inputs to submodules

* haskell-backend/src/main/native/haskell-backend: bd61a0565 - kore-rpc Catch any runtime exception and send as error (#3522)

* Sync flake inputs to submodules

* haskell-backend/src/main/native/haskell-backend: 2020ceb1b - Fixing new nix update breaking cachix installation (#3526)

* Sync flake inputs to submodules

* haskell-backend/src/main/native/haskell-backend: 37f122964 - [#3493] Rename `Fl` (functional) by `T` (total) (#3521)

* Sync flake inputs to submodules

* haskell-backend/src/main/native/haskell-backend: 1c184832b - [#3523] Put unserialized definition.kore in bug report (#3527)

* Sync flake inputs to submodules

* haskell-backend/src/main/native/haskell-backend: 559424aa4 - InfoAttemptUnification to DebugAttemptUnification (#3525)

* Sync flake inputs to submodules

* Fix `Dockerfile`

* Fix another `Dockerfile`

* Update result for failing test

The rename from functional to total changed these outputs

---------

Co-authored-by: rv-jenkins <devops@runtimeverification.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: Tamas Toth <tamas.toth@runtimeverification.com>
Co-authored-by: Radu Mereuta <headness13@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Baltoli @fiedlr