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

Seq vs List Correspondence #1302

Closed
wants to merge 20 commits into from
Closed

Seq vs List Correspondence #1302

wants to merge 20 commits into from

Commits on Sep 20, 2024

  1. Add new functional big-step semantics example for an imperative langu… 

    …age similar to fun-op-sem/imp, but uses lists for sequencing
    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    92a5df0 View commit details
    Browse the repository at this point in the history

  2. Add transformations between fun-op-sem/imp and fun-op-sem/imp2

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    46b894c View commit details
    Browse the repository at this point in the history

  3. Add proofs about fun-op-sem/imp2 size

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    3e8e859 View commit details
    Browse the repository at this point in the history

  4. Add proof that fun-op-sem/imp2 evaluation is monotonic in clock

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    e10afbc View commit details
    Browse the repository at this point in the history

  5. Add proof for how pval distributes over APPEND

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    89cacc9 View commit details
    Browse the repository at this point in the history

  6. Add proof that evaluating fun-op-sem/imp with larger clock results in… 

    … larger clock
    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    50329d8 View commit details
    Browse the repository at this point in the history

  7. Add proof that fun-op-sem/imp evaluation is monotonic in clock

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    7fb55c7 View commit details
    Browse the repository at this point in the history

  8. Add proof that larger resultant clock means evaluated fun-op-sem/imp … 

    …with larger clock
    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    c82fbdf View commit details
    Browse the repository at this point in the history

  9. Add proof that can get any resultant clock above known resultant cloc… 

    …k given appropriate initial clock
    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    a68168b View commit details
    Browse the repository at this point in the history

  10. Add proof that can get any resultant clock given an appropriate initi… 

    …al clock for terminating programs in fun-op-sem/imp
    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    aafc4cb View commit details
    Browse the repository at this point in the history

  11. Add correspondence proofs between fun-op-sem/imp and fun-op-sem/imp2

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    3876af1 View commit details
    Browse the repository at this point in the history

  12. Fix trailing whitespace error

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    5145376 View commit details
    Browse the repository at this point in the history

  13. Remove unused weaker lemma

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    910a7c8 View commit details
    Browse the repository at this point in the history

  14. Make lrg_clk proof more concise

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    833676d View commit details
    Browse the repository at this point in the history

  15. Make lrg_clk2 proof more concise

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    d3fc0fd View commit details
    Browse the repository at this point in the history

  16. Make arb_resc proof more concise

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    5d58756 View commit details
    Browse the repository at this point in the history

  17. Make lrg_clk2 proof more concise

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    9f8116f View commit details
    Browse the repository at this point in the history

  18. Make lrg_clk2 proof more concise

    @adamstucci
    adamstucci committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    3f6247f View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2024

  1. Make lrg_clk proof more concise

    @adamstucci
    adamstucci committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    0a11bf4 View commit details
    Browse the repository at this point in the history

  2. Make cval_mono proof more concise

    @adamstucci
    adamstucci committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    c88c57f View commit details
    Browse the repository at this point in the history